AN AXIOMATIC BASIS FOR COMPUTER PROGRAMMING

被引：2405

作者：

HOARE, CAR

机构：

[1] Queen's Univ., Belfast

来源：

COMMUNICATIONS OF THE ACM | 1969年 / 12卷 / 10期

关键词：

axiomatic method; formal language definition; machine-independent programming; program documentation; programming language design; theory of programming' proofs of programs;

D O I：

10.1145/363235.363259

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

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. © 1969 ACM. All rights reserved.

引用

页码：576 / &