Unrestricted procedure calls in Hoare's logic

ABSTRACT

This paper presents a new version of Hoare's logic including generalized procedure call and assignment rules which correctly handle aliased variables. Formal justifications are given for the new rules.

REFERENCES

• 1: {Apt and DeBakker 77} Apt, K. R. and J. W. DeBakker. Semantics and Proof Theory of PASCAL Procedures, Tech. Rpt., Stichting Mathematisch Centrum, Amsterdam, }977.
• 2: {Cook 75} Cook, S. Axiomatic and Interpretive Semantics for an Algol Fragment, Tech. Rpt. 79, Dept. of Comp. Sci., Univ. of Toronto, Feb., 1975.
• 3: James Edward Donahue, Complementary Definitions of Programming Language Semantics, Springer-Verlag New York, Inc., Secaucus, NJ, 1976
• 4: {Enderton 72} Enderton, H. A Mathematical Introduction to Logic, Academic Press, New York, 1972.
• 5: {Gorelick 75} Gorelick, G. A. A Complete Axiomatic System for Proving Assertions about Recursive and Non-recursive Programs, Tech. Rpt. 75, Dept. of Comp. Sci., Univ. of Toronto, Jan., 1975.
• 6: {Guttag 77} Guttag, J. V., J. J. Horning, and R. L. London. A Proof Rule for EUCLID Procedures, Tech. Rpt., Xerox PARC, Palo Alto, Ca., 1977.
• 7: {Igarashi, London, and Luckham 75} Automatic Program Verification I: A Logical Basis and Its Implementation, Acta Informatica 4 (1975), pp. 145-182.
• 8: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 9: {Hoare 71} Hoare, C. A. R. Procedures and Parameters: An Axiomatic Approach, Symp. on Semantics of Algorithmic Languages, E. Engler (ed.), Springer-Verlag, Berlin, 1971, pp. 102-116.
• 10: {Hoare and Wirth 73} Hoare, C. A. R. and N. Wirth. An Axiomatic Definition of the Programming Language PASCAL, Acta Informatica 1 (1971).
• 11: {London 77} London, R. L., et al. Proof Rules for the Programming Language EUCLID, Tech. Rpt., Xerox PARC, Palo Alto, Ca., 1977.
• 12: {Oppen 75} Oppen, D. C. On Logic and Program Verification, Tech. Rpt. 82, Dept. of Comp. Sci., Univ. of Toronto, 1975.