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 advantage, both theoretical and practical, may follow from a pursuance of these topics.
- 1 YANOV, Yu I. Logical operator schemes. Kybernetika 1, (1958).Google Scholar
- 2 IGARASHI, 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 BAKICER, J. W. Axiomatics of simple assignment statements. M.R. 94, Mathematisch 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 LASKI, 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), 310-316.Google ScholarDigital Library
Index Terms
- An axiomatic basis for computer programming
Recommendations
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 ...
An axiomatic basis for computer programming
Special 25th Anniversary IssueIn 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