An axiomatic basis for computer programming

ABSTRACT

In this paper an attempt is made to explore the logical foundations of computer programming by use of techniques which were first applied in the study of geometry and have later been extended to other branches of mathematics. This involves the elucidation of sets of axioms and rules of inference which can be used in proofs of the properties of computer programs. Examples are given of such axioms and rules, and a formal proof of a simple theorem is displayed. Finally, it is argued that important advantages, both theoretical and practical, may follow from a pursuance of these topics.

REFERENCES

• 1: YANOV, YU I. Logical operator schemes. Kybernetika I, (1958).
• 2: IGARASHX, S. An axiomatic approach to equivalence problems of algorithms with applications. Ph.D. Thesis 1964. Rep. Compt. Centre, U. Tokyo, 1968, pp. 1-101.
• 3: DE BAKKEa, J. W. Axiomaties of simple assignment statements. M.R. 94, Mathematiseh Centrum, Amsterdam, June 1968.
• 4: MCCARTHY, J. Towards a mathematical theory of computation. Proc. IFIP Cong. 1962, North Holland Pub. Co., Amsterdam, 1963.
• 5: BURSTALL, R. Proving properties of programs by structural induction. Experimental Programming Reports: No. 17 DMIP, Edinburgh, Feb. 1968.
• 6: VAN WIJNGAARDEN, A. Numerical analysis as an independent science. BIT 6 (1966), 66-81.
• 7: J. G Laski, Sets and other types, ALGOL Bulletin [doi>10.1145/1061098.1061107]
• 8: FLOYD, R. W. Assigning meanings to programs. Proc. Amer. Math. Soc. Symposia in Applied Mathematics, Vol. 19, pp. 19-31.
• 9: NAUR, P. Proof of algorithms by general snapshots. BIT 6 (1966), 316-316.
• 1: Davis, M. Computability and Unsolvability. McGraw-Hill Book Company, New York, 1958.
• 2: SAMELSONI K. Programming languages and their processing. Proceedings, IFIP Congress, 1962, North-Holland Publishing Co., Amsterdam, 1963, p. 487.

INDEX TERMS

Keywords:
axiomatic method, formal language definition, machine-independent programming, program documentation, programming language design, proofs of program, proofs of programs, theory of programming