Article

Free access

Abstractions, instantiations, and proofs of marking algorithms

Authors:

Lawrence Yelowitz,

Arthur G. DuncanAuthors Info & Claims

Proceedings of the 1977 symposium on Artificial intelligence and programming languages

Pages 13 - 21

https://doi.org/10.1145/800228.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

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
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

Proceedings of the 1977 symposium on Artificial intelligence and programming languages

August 1977

185 pages

ISBN:9781450378741

DOI:10.1145/800228

Chairman:
James Low

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
ACM SIGART Bulletin Just Accepted
Proceedings of the 1977 symposium on Artificial intelligence and programming languages
August 1977
179 pages
ISSN:0163-5719
DOI:10.1145/872736
Issue’s Table of Contents

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 August 1977

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

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
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
Duncan AYelowitz L(2005)Studies in abstract/concrete mappings in proving algorithm correctnessAutomata, Languages and Programming10.1007/3-540-09510-1_17(218-229)Online publication date: 25-May-2005
https://doi.org/10.1007/3-540-09510-1_17

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.

Cited By

Index Terms

Recommendations

Abstractions, instantiations, and proofs of marking algorithms

Abstractions, instantiations, and proofs of marking algorithms

Array abstractions from proofs