article

Free access

Abstractions, instantiations, and proofs of marking algorithms

Authors:

Lawrence Yelowitz,

Arthur G. DuncanAuthors Info & Claims

ACM SIGPLAN Notices, Volume 12, Issue 8

Pages 13 - 21

https://doi.org/10.1145/872734.806927

Published: 01 August 1977 Publication History

PDF eReader

Abstract

A detailed look is taken at the problem of factoring program proofs into a proof of the underlying algorithm, followed by a proof of correct implementation of abstract variables at the concrete level. We do this considering four different concrete “marking” algorithms and formulating a single abstract algorithm and set of abstract specifications that can be instantiated to each of the four concrete cases. An intermediate assertion, as well as sufficient conditions for correct initialization, invariance, and correctness at termination are given at the abstract level. Proofs at the concrete level are then given by exhibiting appropriate mapping functions (from the concrete state vector to the abstract variables), and showing that the sufficient conditions are true. Proofs of termination are given by instantiating “termination schemas”.

References

[1]

Dijkstra, E. W., A discipline of programming, Prentice-Hall, 1976.

Digital Library

Google Scholar

[2]

Duncan, A. G., Studies in program correctness, Ph.D. dissertation, University of California, Irvine, May 1976.

Digital Library

Google Scholar

[3]

Floyd, R. W., Assigning meanings to programs, Proceedings of a Symposium in Applied Mathematics 19, (ed. Schwartz, J. T.), Providence, Rhode Island: American Mathematical Society, 1967, pp. 19-32.

Google Scholar

[4]

Gerhart, S., and Yelowitz, L., Control structure abstractions of the backtracking programming technique, IEEE Transactions on Software Engineering, vol. SE-2, no. 4, Dec. 1976, pp. 285-292.

Digital Library

Google Scholar

[5]

Gerhart, S. L., Abstractions and proofs of marking algorithms, (private correspondence).

Google Scholar

[6]

Knuth, D. E., The Art of Computer Programming, vol. 1, Fundamental Algorithms, Addison-Wesley, 1973.

Digital Library

Google Scholar

[7]

Morris, J. H., Verification-oriented language design, Technical Report 7, Computer Science Dept. U. of California, Berkeley, Dec. 1972.

Google Scholar

[8]

Schorre, H., and Waite, W., An efficient machine-independent procedure for garbage collection in various list structures, CACM 10.

Digital Library

Google Scholar

[9]

Suzuki, N., Automatic verification of programs with complex data structures, Stanford U. Computer Science Dept. Report No. STAN-CS-76-552, Feb. 1976 (Ph.D. dissertation)

Digital Library

Google Scholar

[10]

Topor, R., The correctness of the Schorre-Waite list marking algorithm, Report MIP-R-104, School of Artificial Intelligence, U. of Edinburgh, July 1974.

Google Scholar

[11]

Yelowitz, L., A symmetric, top-down structured approach to computer program/proof development, Ph.D. dissertation, The Johns Hopkins University, May 1972, published as IBM Technical Report FSC 73-5001, Bethesda, Maryland, July 1973.

Digital Library

Google Scholar

[12]

Yelowitz, L., and Duncan, A. G., Data structures and program correctness: bridging the gap, Proceedings of the 1977 Conference on Information Sciences and Systems, March 30-April 1, 1977, sponsored by the Dept. of Electrical Engineering, The Johns Hopkins University, pp. 113-117.

Google Scholar

[13]

Wulf, W. A., London, R. L., and Shaw, M., An introduction to the construction and verification of Alphard programs, IEEETSE SE-2, 4, Dec. 1976, pp. 253-265.

Digital Library

Google Scholar

Cited By

View all

Ward M(1996)Derivation of Data Intensive Algorithms by Formal TransformationIEEE Transactions on Software Engineering10.1109/32.54143722:9(665-686)Online publication date: 1-Sep-1996
https://dl.acm.org/doi/10.1109/32.541437
Loginov AReps TSagiv M(2006)Automated verification of the deutsch-schorr-waite tree-traversal algorithmProceedings of the 13th international conference on Static Analysis10.1007/11823230_17(261-279)Online publication date: 29-Aug-2006
https://dl.acm.org/doi/10.1007/11823230_17
Gerhart S(2005)A derivation-oriented proof of the Schorr-Waite marking algorithmProgram Construction10.1007/BFb0014678(472-492)Online publication date: 9-Jun-2005
https://doi.org/10.1007/BFb0014678
Show More Cited By

Index Terms

Abstractions, instantiations, and proofs of marking algorithms

Recommendations

Abstractions, instantiations, and proofs of marking algorithms
Proceedings of the 1977 symposium on Artificial intelligence and programming languages

A detailed look is taken at the problem of factoring program proofs into a proof of the underlying algorithm, followed by a proof of correct implementation of abstract variables at the concrete level. We do this considering four different concrete “...
Abstractions, instantiations, and proofs of marking algorithms
Proceedings of the 1977 symposium on Artificial intelligence and programming languages

A detailed look is taken at the problem of factoring program proofs into a proof of the underlying algorithm, followed by a proof of correct implementation of abstract variables at the concrete level. We do this considering four different concrete “...
Array abstractions from proofs
CAV'07: Proceedings of the 19th international conference on Computer aided verification

We present a technique for using infeasible program paths to automatically infer Range Predicates that describe properties of unbounded array segments. First, we build proofs showing the infeasibility of the paths, using axioms that precisely encode the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACM SIGPLAN Notices Volume 12, Issue 8

Proceedings of the 1977 symposium on Artificial intelligence and programming languages

August 1977

179 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/872734

Issue’s Table of Contents

Proceedings of the 1977 symposium on Artificial intelligence and programming languages
August 1977
185 pages
ISBN:9781450378741
DOI:10.1145/800228
Chairman:
James Low

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 August 1977

Published in SIGPLAN Volume 12, Issue 8

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
296
Total Downloads

Downloads (Last 12 months)81
Downloads (Last 6 weeks)9

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Ward M(1996)Derivation of Data Intensive Algorithms by Formal TransformationIEEE Transactions on Software Engineering10.1109/32.54143722:9(665-686)Online publication date: 1-Sep-1996
https://dl.acm.org/doi/10.1109/32.541437
Loginov AReps TSagiv M(2006)Automated verification of the deutsch-schorr-waite tree-traversal algorithmProceedings of the 13th international conference on Static Analysis10.1007/11823230_17(261-279)Online publication date: 29-Aug-2006
https://dl.acm.org/doi/10.1007/11823230_17
Gerhart S(2005)A derivation-oriented proof of the Schorr-Waite marking algorithmProgram Construction10.1007/BFb0014678(472-492)Online publication date: 9-Jun-2005
https://doi.org/10.1007/BFb0014678
Sankaran N(1994)A bibliography on garbage collection and related topicsACM SIGPLAN Notices10.1145/185009.18504029:9(149-158)Online publication date: 1-Sep-1994
https://dl.acm.org/doi/10.1145/185009.185040
Dershowitz N(1985)Program abstraction and instantiationACM Transactions on Programming Languages and Systems10.1145/3916.39867:3(446-477)Online publication date: 1-Jul-1985
https://dl.acm.org/doi/10.1145/3916.3986
Back RMannila HRäihä KWhite JLandweber LDemers ATeitelbaum T(1983)Derivation of efficient DAG marking algorithmsProceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages10.1145/567067.567071(20-27)Online publication date: 24-Jan-1983
https://dl.acm.org/doi/10.1145/567067.567071
Dershowitz NJeffrey SStucki L(1981)The evolution of programsProceedings of the 5th international conference on Software engineering10.5555/800078.802519(79-88)Online publication date: 9-Mar-1981
https://dl.acm.org/doi/10.5555/800078.802519
Lee SdeRoever WGerhart SAho AZilles SRosen B(1979)The evolution of list-copying algorithms and the need for structured program verificationProceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages10.1145/567752.567758(53-67)Online publication date: 1-Jan-1979
https://dl.acm.org/doi/10.1145/567752.567758

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Cited By

Index Terms

Recommendations