コンピュータ・プログラミングの公理的基礎
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