C. A. R. Hoare
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.
- 1 YANOV, YU I. Logical operator schemes. Kybernetika I, (1958).Google Scholar
- 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.Google Scholar
- 3 DE BAKKEa, J. W. Axiomaties of simple assignment statements. M.R. 94, Mathematiseh Centrum, Amsterdam, June 1968.Google Scholar
- 4 MCCARTHY, J. Towards a mathematical theory of computation. Proc. IFIP Cong. 1962, North Holland Pub. Co., Amsterdam, 1963.Google Scholar
- 5 BURSTALL, R. Proving properties of programs by structural induction. Experimental Programming Reports: No. 17 DMIP, Edinburgh, Feb. 1968.Google Scholar
- 6 VAN WIJNGAARDEN, A. Numerical analysis as an independent science. BIT 6 (1966), 66-81.Google ScholarCross Ref
- 7 LASET, J. Sets and other types. ALGOL Bull. 27,1968. Google ScholarDigital Library
- 8 FLOYD, R. W. Assigning meanings to programs. Proc. Amer. Math. Soc. Symposia in Applied Mathematics, Vol. 19, pp. 19-31.Google ScholarCross Ref
- 9 NAUR, P. Proof of algorithms by general snapshots. BIT 6 (1966), 316-316.Google ScholarCross Ref
- 1 Davis, M. Computability and Unsolvability. McGraw-Hill Book Company, New York, 1958.Google Scholar
- 2 SAMELSONI K. Programming languages and their processing. Proceedings, IFIP Congress, 1962, North-Holland Publishing Co., Amsterdam, 1963, p. 487.Google Scholar
Index Terms
- An axiomatic basis for computer programming
Recommendations
An axiomatic basis for computer programming
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 ...
An axiomatic basis for computer programming
Software pioneersIn 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 ...
A comment on axiomatic approaches to programming
Reference is made to the paper by C. A. R. Hoare [1] which discusses the fundamentals of an axiomatic approach to computer programming. One advantage for an axiomatic system proposed by Hoare is that an axiomatic description of computer programs would ...
Comments