Summary
We present a new version of Hoare's logic that correctly handles programs with aliased variables. The central proof rules of the logic (procedure call and assignment) are proved sound and complete.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Apt, K.R., DeBakker, J.W.: Semantics and proof theory of PASCAL procedures. Tech. Rept., Stichting Mathematsch Centrum, Amsterdam, 1977
Clarke, E.M.: Programming language constructs for which it is impossible to obtain good Hoare-like axiom systems. Proceedings of Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, 1976
Cook, S.: Axiomatic and Interpretive Semantics for an Algol Fragment. Tech. Rpt. 79, Dept. of Comp. Sci., Univ. of Toronto, 1975
Dijkstra, E.: A discipline of programming. Englewood Cliffs, N.J.: Prentice-Hall 1976
Donahue, J.E.: Complementary definitions of programming language semantics. Berlin Heidelberg New York: Springer 1976
Enderton, H.: A mathematical introduction to logic. New York: Academic Press 1972
Gorelick, G.A.: A complete axiomatic system for proving assertions about recursive and nonrecursive programs. Tech. Rpt. 75, Dept. of Comp. Sci., Univ. of Toronto, 1975
Gries, D.: The multiple assignment statement. IEEE Trans. Software Engrg. SE-4, 89–93 (1978)
Hoare, C.A.R.: An axiomatic approach to computer programming. CACM 12, 332–329 (1969)
Hoare, C.A.R.: Procedures and parameters: An axiomatic approach. In: Symposium on semantics of algorithmic languages (E. Engeler, ed.), Lecture Notes in Mathematics, Vol. 188, pp. 102–116. Berlin Heidelberg New York: Springer 1971
Igarashi, S., London, R., Luckham, D.: Automatic program verification I: a logical basis and its implementation. Acta Informat. 4, 145–182 (1975)
London, R.L., Guttag, J.V., Horning, J.J., Lampson, B.W., Mitchell, J.G., Popek, G.J.: Proof rules for the programming language EUCLID. Acta Informat. 10, 1–26 (1976)
McCarthy, J.: A basis for a mathematical theory of computation. In: Computing programming and formal systems (P. Braffort, D. Hirshberg, eds.). Amsterdam: North-Holland 1963
Nelson, C.G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Programming Languages Systems, 2, 245–257 (1979)
Oppen, D.C.: On logic and program verification. Tech. Rpt. 82, Dept. of Comp. Sci., Univ. of Toronto, 1975
Pratt, V.R.: Semantical considerations on Floyd-Hoare logic, 17th Symposium on Foundations of Computer Science, IEEE, October 1976
Wirth, N.: The programming language PASCAL. Acta Informat. 1, 35–63 (1971)
Author information
Authors and Affiliations
Additional information
An earlier version of this paper appeared in the Proceedings of the Fifth ACM Symposium on Principles of Programming Languages, 1978. This research has been partially supported by National Science Foundation grants MCS 76-14293 and MCS 76-000327
Rights and permissions
About this article
Cite this article
Cartwright, R., Oppen, D. The logic of aliasing. Acta Informatica 15, 365–384 (1981). https://doi.org/10.1007/BF00264535
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00264535