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 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.

KEY WORDS AND PHRASES: axiomatic method, theory of programming’ proofs of programs, formal language definition, programming language design, machine-independent programming, program documentation CR CATEGORY: 4.0, 4.21, 4.22, 5.20, 5.21, 5.23, 5.24

计算机程序设计的公理基础

C. A. R. Hoare 贝尔法斯特女王大学，* 北爱尔兰

本文试图运用最初应用于几何学研究、后来扩展到数学其他分支的技术，探索计算机程序设计的逻辑基础。这涉及阐明一组公理和推理规则，可用于证明计算机程序的性质。文中给出了这类公理和规则的实例，并展示了一个简单定理的形式化证明。最后，本文指出，继续开展这些研究可能带来重要的理论和实践益处。

关键词和短语：公理化方法，程序设计理论，程序证明，形式化语言定义，编程语言设计，机器无关的程序设计，程序文档 CR 分类：4.0，4.21，4.22，5.20，5.21，5.23，5.24

1 Introduction

This section is missing here.

2 Computer Arithmetic

This section is missing here.

3 Program Execution

This section is missing here.

4 General Reservations

This section is missing here.

5 Proofs of Program Correctness

This section is missing here.

Notes

This section is missing here.

6 Formal Language Definition

This section is missing here.