Side effects and aliasing can have simple axiomatic descriptions

ABSTRACT

We present a different style of axiomatic definition for programming languages. It is oriented toward imperative languages, such as Algol 68, that do not distinguish between statements and expressions. Rather than basing the logic on a notion of pre- or postcondition, we use the value of a programming language expression as the underlying primitive. A number of language constructs are examined in this framework. We argue that this style of definition gives us a significantly different view of the notion of “easy axiomatixability.” Side effects in expressions as well as aliasing between variables are shown to be “easily axiomatizable” in our system.

REFERENCES

• 1: Hans-J. Boehm, A logic for expressions with side-effects, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.268-280, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582182]
• 2: Hans-Juergen Karl Hermann Boehm, A logic for the russell programming language, 1984
• 3: BOEHM, H.-J., DEMERS, A., AND DONAHUE, J. A programmer's introduction to Russell. Tech. Rep. 85-16, Dept. of Computer Science, Rice Univ., 1985. See also {12}.
• 4: BOYER, R. S., ANO STROTHER MOORE, J. A Computational Logic. Academic Press, New York, 1979.
• 5: BROOKES, S.D. A fully abstract semantics and a proof system for an Algol-like language with sharing. Tech. Rep. CMU-CS-84-118A, Dept. of Computer Science, Carnegie-Mellon Univ., Feb. 1985.
• 6: CARTWRIGHT, R., AND OPPEN, D. The logic of aliasing. Acta Inf. 15 (1981), 365-384.
• 7: Edmund Melson Clarke, Jr., Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems, Journal of the ACM (JACM), v.26 n.1, p.129-147, Jan. 1979 [doi>10.1145/322108.322121]
• 8: 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]
• 9: CONSTABLE, R. L., AND O'DONNELL, M.J. A Programming Logic. Winthrop, Cambridge, 1978.
• 10: COOK, S. Soundness and completeness of an axiom system for program verification. Tech. Rep. 95, Dept. of Computer Science, Univ. of Toronto, June 1976.
• 11: CUNNINGHAM, R. J., ANO GILFORD, M. E.J. A note on the semantic definition of side effects. Inf. Process. Lett. 4, 5 (Feb. 1976), 118-120.
• 12: DEMERS, A. J., ANO DONAHUE, J. E. Data types are values. Tech. Rep. 79-393, Dept. of Computer Science, Cornell Univ., 1979.
• 13: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 14: 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]
• 15: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• 16: David Harel, First-Order Dynamic Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1979
• 17: Eric C. R. Hehner, Predicative programming Part I, Communications of the ACM, v.27 n.2, p.134-143, Feb. 1984 [doi>10.1145/69610.357988]
• 18: 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]
• 19: K Jensen , N Wirth , A B Mickel , J F Miner, Pascal user manual and report; 3rd ed., Springer-Verlag New York, Inc., New York, NY, 1985
• 20: KOWALTOWSKI, T. Axiomatic approach to side effects and general jumps. Acta Inf. 7, 4 (1977), 357-360.
• 21: McCARTHY, J. A basis for a mathematical theory of computation. In Computer Programming and Formal Systems, P. Braffort and D. Hirschberg, Eds., North-Holland, Amsterdam, 1963. See also {24}.
• 22: MIRKOWSKA, G. On formalized systems of algorithmic logic. Bull. de L'Academie Polonaise des Sciences, Serie des Sciences Math., Astr. et Phys. 19, 6 (1971), 421-428.
• 23: Michael J. O'Donnell, A critique of the foundations of Hoare style programming logics, Communications of the ACM, v.25 n.12, p.927-935, Dec 1982 [doi>10.1145/358728.358748]
• 24: PARK, D. Fixpoint induction and proofs of program properties. Mach. lntell. 5, American Elsevier, New York, 1970, 59-78.
• 25: G. J. Popek , J. J. Horning , B. W. Lampson , J. G. Mitchell , R. L. London, Notes on the design of Euclid, Proceedings of an ACM conference on Language design for reliable software, p.11-18, March 28-30, 1977, Raleigh, North Carolina
• 26: PRITCHARD, P. Program proving--expression languages. In Information Processing 77, North- Holland, Amsterdam, 1977, 727-731. For more details see: An axiomatic semantics for expression languages. Thesis, Australian National Univ., Nov. 1979. Available as a joint technical report from the Computer Science Depts. at the Australian National Univ. (TR-CS-80-11) and the Univ. of Queensland (TR-20).
• 27: SCHWARTZ, R.L. An axiomatic treatment of asynchronous processes in Algol 68. Preliminary draft. More details can be found in: An axiomatic semantic definition of Algol 68, Computer Science Dept., UCLA-34P214-75, Univ. of California, Los Angeles, July 1978.
• 28: VAN WIJNGAARDEN, A., MAILLOUX, B. J., PECK, J. E. L., KOSTER, C. H. A., SINTZOr~, M., LINDSEY, C. H., MEERTENS, L. G. L. T., AND FISKER, R.G. Revised report on the algorithmic language Algol 68. Acta Inf. 5, 1-3 (1975), 1-236.
• 29: WULr, W. A., ET AL. BLISS-11 Programmer's Manual. Digital Equipment Corp., Maynard, Mass., 1972.

INDEX TERMS

Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs; Mechanical verification

General Terms:
Languages, Theory, Verification