Abstract
This paper discusses the problem of factoring program proofs into a proof of correctness of an abstract algorithm followed by a proof of correct implementation at the concrete level. The problem of showing that diagrams commute is simplified by the introduction of a set of abstract entities that define constraints on the abstract operations. Correctness at the concrete level is then shown by exhibiting two appropriate mappings, CA (from the concrete state space to the abstract state space) and CE (from the concrete state space to the set of abstract entities).
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Bibliography
Floyd, R. W., Assigning meanings to programs, Proceedings of a Symposium in Applied Mathematics, 19, (ed. Schwartz, J. T.), Providence Island: American Mathematical Society, 1967, pp. 19–32.
Manna, Z., Properties of programs and the first-order predicate calculus, JACM, 16, 1969, pp. 244–255.
Hoare, C.A.R., An axiomatic basis for computer programming, CACM 12, 1969, pp. 576–580, 583.
Dijkstra, E. W., A discipline of programming, Prentice-Hall, Inc., Englewood Cliffs, NJ, 1976.
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.
Milner, R., An algebraic definition of simulation between programs, Report No. CS-205, Computer Science Dept., Stanford University, Feb. 1971.
Birman, A. and Joyner, W. H., A Problem-Reduction Approach to Proving Simulation between Programs, IEEETSE SE-2, 2, June 1976.
Knuth, D. E., The art of computer programming, v. 1, Fundamental algorithms, Addison-Wesley Publishing Co., Reading, Mass., 1972–1973.
Schorr, H., and Waite, W., An efficient machine-independent procedure for garbage collection in various list structures, CACM 10.
Yelowtitz, L., and Duncan, A. G., Abstractions, instantiations, and proofs of marking algorithms, in Proceedings of the Symposium on Artificial Intelligence and Programming Languages, SIGPLAN Notices, 12, 8 and SIGART Newsletter no. 64, August 1977, pp. 13–21.
Topor, T., The correctness of the Schorr-Waite list marking algorithm, Report MIP-R-104, School of Artificial Intelligence, University of Edinburgh, July 1974.
Duncan, A. G., Studies in Program Correctness, Ph. D. Dissertation, University of California, Irvine, 1976.
Yelowitz, L. and Duncan, A. G., Data Structures and Program Correctness: Bridging the Gap, Computer Languages, v. 3, 1978.
Lee, S., deRoever, W. P. and Gerhart, S. L., The Evolution of List-Copying Algorithms, Proceedings of the Sixth ACM Symposium on Principles of Programming Languages, January 1979.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1979 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Duncan, A.G., Yelowitz, L. (1979). Studies in abstract/concrete mappings in proving algorithm correctness. In: Maurer, H.A. (eds) Automata, Languages and Programming. ICALP 1979. Lecture Notes in Computer Science, vol 71. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-09510-1_17
Download citation
DOI: https://doi.org/10.1007/3-540-09510-1_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-09510-1
Online ISBN: 978-3-540-35168-9
eBook Packages: Springer Book Archive