Axiomatic definitions of programming languages: a theoretical assessment (preliminary report)

ABSTRACT

A precise definition is given of how partial correctness or termination assertions serve to specify the semantics of classes of program schemes. Assertions involving only formulas of first order predicate calculus are proved capable of specifying program scheme semantics, and effective axiom systems for deriving such assertions are described. Such axiomatic specifications are possible despite the limited expressive power of predicate calculus.

REFERENCES

• 1: Apt, K. R., J. A. Bergstra, L. G. L. T. Meertens. Recursive Assertions Are Not Enough - Or Are They? Theoretical Computer Science, in vol. 8, pp. 73-87, 1979.
• 2: Bergstra, J. A., J. Tiuryn, and J. V. Tucker. Correctness Theories and Program Equivalence. Preprint. Stichting Mathematisch Centrum, Amsterdam, 1979.
• 3: Cook, S. A. Soundness and Completeness of an Axiom System for Program Verification. SIAM Journal on Computing, vol. 7, no. 1. February, 1978.
• 4: Edsger W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, v.18 n.8, p.453-457, Aug. 1975 [doi>10.1145/360933.360975]
• 5: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 6: Floyd, R. W. Assigning Meaning to Programs. In Mathematical Aspects of Computer Science. Proceedings of Symposium in Applied Mathematics (ed. J. T. Schwartz). (pp. 19-33) American Math. Society, Providence, Rhode Island, 1967.
• 7: Friedman, H. Algorithmic Procedures, Generalized Turing Algorithms, and Elementary Recursion Theory. In Logic colloquiuum, 1969 (ed. R. O. Gandy and C. M. E. Yates) (pp. 316-389). North Holland, Amsterdam, 1971.
• 8: Greif, I. and A. R. Meyer. Specifying the Semantics of While-Programs. M.I.T., Laboratory for Computer Science, TM-130. M.I.T., Cambridge, Mass. 02139, April, 1979.
• 9: D. Harel, LOGICS OF PROGRAMS: AXIOMATICS AND DESCRIPTIVE POWER, Massachusetts Institute of Technology, Cambridge, MA, 1978
• 10: D. Harel , A. R. Meyer , V. R. Pratt, Computability and completeness in logics of programs (Preliminary Report), Proceedings of the ninth annual ACM symposium on Theory of computing, p.261-268, May 04-04, 1977, Boulder, Colorado, United States [doi>10.1145/800105.803416]
• 11: Hoare, C. A. R. and P. Lauer. Consistent and Complementary Formal Theories of the Semantics of Programming Languages. Acta Informatica 3, pp 135-155, 1974.
• 12: Hoare, C. A. R. and N. Wirth. An Axiomatic Definition of the Programming Language PASCAL. Acta Informatica 2, pp. 335-355, 1973.
• 13: Janssen, T. M. V. and P. van Emde Boas. The Expressive Power of Intensional Logic in the Semantics of Programming Languages. Preprint. Stichting Mathematisch Centrum, Amsterdam, May, 1977.
• 14: Kleene, S. C. Two Papers on the Predicate Calculus. Memoirs of the American Math. Soc., No. 10. (pp. 27-66). American Math. Society Providence, Rhode Island, 1952.
• 15: London, Ralph L. Program Verification In Research Directions in Software Technology. ed. Peter Wegner. (pp. 302-315). M.I.T. Press, Cambridge, Mass., 1978.
• 16: Michael Machtey , Paul Young, An Introduction to the General Theory of Algorithms, Elsevier Science Inc., New York, NY, 1978
• 17: Pratt, V. R. Semantical Considerations of Floyd-Hoare Logic. 17th Annual IEEE Symposium on the Foundations of Computer Science. pp. 109-121, October, 1976.
• 18: Schwartz, R. An Axiomatic Semantic Definition of Algol 68. UCLA-ENG-7838; UCLA-34P214-75, University of California at Los Angeles, Los Angeles, Calif. 1978.