A logic for expressions with side-effects

ABSTRACT

This paper presents a simple programming logic LES, which is particularly well suited for reasoning about so-called expression languages, i.e. languages that incorporate imperative features into expressions rather than distinguishing between expressions and statements. An axiomatization of a simple programming language is presented using this formalism. It is shown that this axiomatization is relatively complete, roughly in the sense of [Coo 76].

REFERENCES

• 1: Robert Cartwright , Derek Oppen, The Logic of Aliasing, Cornell University, Ithaca, NY, 1978
• 2: Robert L. Constable, On the theory of programming logics, Proceedings of the ninth annual ACM symposium on Theory of computing, p.269-285, May 04-04, 1977, Boulder, Colorado, United States [doi>10.1145/800105.803417]
• 3: {Coo 76} Cook, Stephen A., "Soundness and Completeness of an Axiom System for Program Verification", Department of Computer Science, University of Toronto, Technical Report No. 95, June 1976.
• 4: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 5: David Gries , Gary Levin, Assignment and Procedure Call Proof Rules, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.4, p.564-579, Oct. 1980 [doi>10.1145/357114.357119]
• 6: David Harel, First-Order Dynamic Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1979
• 7: 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]
• 8: {Kow 77} Kowaltowski, Tomasz, "Axiomatic Approach to Side Effects and General Jumps", Acta Informatica 7, pp. 357--360, 1977.
• 9: {Pri 77} Pritchard, Paul, "Program Proving --- Expression Languages", Information Processing 77, North Holland, 1977, pp. 727--731.
• 10: {Schw 78} Schwartz, Richard L., "An Axiomatic Treatment of Asynchromous Processes in ALGOL 68", preliminary draft. More detail can be found in: Schwartz, Richard L. "An Axiomatic Semantic Definition of ALGOL 68", Computer Science Department, UCLA --- 34P214-75, University of California, Los Angeles, July 1978.