An axiomatic basis for computer programming

Communications of the ACM - Tập 12 Số 10 - Trang 576-580 - 1969
C. A. R. Hoare1
1Queen's Univ. of Belfast, Northern Ireland

Tóm tắt

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.

Từ khóa


Tài liệu tham khảo

YANOV Yu I, 1958, Logical operator schemes, Kybernetika, 1

IGARASHI S, 1968, An axiomatic approach to equivalence problems of algorithms with applications. Ph.D. Thesis 1964. Rep. Compt. Centre, U. Tokyo, 1

DE BAKICER J. W., 1968, Mathematisch Centrum

CARTHY J., 1963, Proc. IFIP Cong. 1962

BURSTALL R., 1968, 17 DMIP

10.1007/BF01939551

10.1145/1061098.1061107

10.1090/psapm/019/0235771

10.1007/BF01966091

Thông tin
Thông tin xuất bản

Communications of the ACM

Tập 12 Số 10

576-580

Thông tin tác giả