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 The Queen’s University of Belfast,* Northern Ireland

本論文では、幾何学の研究に最初に適用され、その後数学の他の分野へ拡張された技法を用いて、コンピュータ・プログラミングの論理的基礎を探究する試みを行う。これには、コンピュータ・プログラムの性質の証明に使用できる公理系および推論規則の集合を明らかにすることが含まれる。このような公理および規則の例を示し、単純な定理の形式的証明を提示する。最後に、これらの問題を追究することによって、理論上および実用上の両面で重要な利点が得られる可能性があることを論じる。

主要語および句：公理的方法、プログラミングの理論、プログラムの証明、形式的な言語定義、プログラミング言語設計、機械に依存しないプログラミング、プログラム文書化 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.