Programming language constructs for which it is impossible to obtain good hoare-like axiom systems

ABSTRACT

Hoare-like deduction systems for establishing partial correctness of programs may fail to be complete because of (a) incompleteness of the assertion language relative to the underlying interpretation or (b) inability of the assertion language to express the invariants of loops. S. Cook has shown that if there is a complete proof system for the assertion language (e.g. all true statements of the assertion language) and if the assertion language satisfies a certain natural expressibility condition, then sound and complete axiom systems for a fairly large subset of Algol may be devised. We exhibit programming language constructs for which it is impossible to obtain sound and complete sets of Hoare-like axioms even in this special sense of Cook's. These constructs include (i) recursive procedures with procedure parameters in a programming language which uses static scope of identifiers and (ii) coroutines in a language which allows parameterless recursive procedures. Modifications of these constructs for which it is possible to obtain sound and complete systems of axioms are also discussed.

REFERENCES

• 1: {CK76} Clarke, Jr., E. M. Programming Language Constructs for Which it is Impossible to Obtain Good Hoare-like Axioms. Technical Report No. 76-287, Computer Science Department, Cornell Univ., August 1976.
• 2: {CK76a} Clarke, Jr., E. M. Pathological Interaction of Programming Language Features. Technical Report CS-1976-15, Computer Science Dept., Duke University, Sept. 1976.
• 3: {CL75} Clint, M. Program Proving: Coroutines. Acta Information, Vol. 2, pp. 50-63, 1973.
• 4: {CO75} Cook, S. A. Axiomatic and Interpretative Semantics for an Algol Fragment. Technical Report 79, Computer Science Dept., University of Toronto, 1975 (to be published in SCICOMP).
• 5: {DE73} deBakker, J. W. and L. G. L. Th. Meertens. On the Completeness of the Inductive Assertion Method. Mathematical Centre, Dec. 1973.
• 6: {DO74} Donahue, James. Mathematical Semantics as a Complementary Definition for Axiomatically Defined Programming Language Constructs, in Donahue et al., Three Approaches to Reliable Software: Language Design, Dyadic Specification, Complementary Semantics. Technical Report CSRG-45, Computer Systems Research Group, University of Toronto, Dec. 1974.
• 7: {GO75} Gorelick, G. A Complete Axiomatic System for Proving Assertions about Recursive and Non-recursive Programs. Technical Report No. 75, Computer Science Dept., University of Toronto, Jan. 1975.
• 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: {HO71} Hoare, C. A. R. Procedures and Parameters: An Axiomatic Approach. Symposium on Semantics of Algorithmic Languages, E. Engeler, Ed., Springer-Verlag, Berlin, pp. 102-116, 1971.
• 10: {HO74} Hoare, C. A. R. and P. E. Lauer. Consistent and Complementary Formal Theories of the Semantics of Programming Languages. Acta Informatica, Vol. 3, pp. 135-154, 1974.
• 11: Neil D. Jones , Steven S. Muchnick, Even Simple Programs Are Hard To Analyze, Journal of the ACM (JACM), v.24 n.2, p.338-350, April 1977 [doi>10.1145/322003.322016]