# An Axiomatic Basis for Computer Programming > [!abstract] 概要 > 本論文では、幾何学の研究で最初に適用され、のちに数学の他の分野へと拡張された技法を用いることによって、コンピュータプログラミングの論理的基礎を探究する試みがなされる。これには、コンピュータプログラムの性質の証明において使用できる公理集合および推論規則の解明が含まれる。そのような公理と規則の例が提示され、単純な定理の形式的証明が示される。最後に、これらの主題の探究から、理論的および実践的な双方の重要な利点が生じうる論拠が述べられる。 ## 論文情報 - タイトル: An Axiomatic Basis for Computer Programming - 著者: C. A. R. Hoare ([[C. A. R. Hoare]]) - 所属: The Queen's University of Belfast, Department of Computer Science ([[Queen's University Belfast]]) - 媒体: Communications of the ACM (CACM), Volume 12, Number 10, pp. 576–580, 583 - 出版年月: 1969年10月（受付: 1968年11月、改訂: 1969年5月） - DOI: 10.1145/363235.363259 ## 概要 本論文は、数理論理学の公理的方法（公理系と推論規則）をプログラミング言語のテキストに直接適用し、プログラムの正しさの形式的証明を可能にする理論的枠組み（のちに[[公理的意味論|ホーア論理]]、[[公理的意味論]]と呼ばれる体系）を提唱した古典的論文である。Robert W. Floyd ([[Robert W. Floyd]]) がフローチャートに対して考案した表明法をプログラムのテキスト構文へと発展させ、代入公理スキーマ、合成規則、反復規則、帰結規則を定式化した。さらに、$P\\{Q\\}R$（事前条件 $P$ が成立してプログラム $Q$ が開始されれば、停止時に事後条件 $R$ が成立する）という記法を導入し、整数除算プログラムの部分正当性の形式的証明を具体例として提示した。また、プログラミング言語の意味論定義に公理的アプローチを用いる利点として、信頼性の向上、プログラム文書化の厳密化、実装非依存の互換性確保、未定義動作の柔軟な仕様化、より明晰な言語設計を挙げている。 ## 問題設定 1. **プログラミングにおける演繹的推論の欠如**: コンピュータプログラミングは、プログラムの全性質や実行結果がテキスト自体から純粋な演繹的推論によって見出せる精密科学（exact science）であるはずだが、従来のプログラミング推論の基礎となる公理や推論規則が明確にされていなかった。 2. **計算機演算と数学的算術の乖離**: 計算機で扱われる演算（特に整数演算）は、数学における無限集合上の算術とは異なり有限集合であり、オーバーフロー時の挙動（計算停止・上限打止め・剰余計算）によって性質が異なる。そのため、プログラムが依存する演算の公理的性質を注意深く選定・形式化する必要があった。 3. **テスト依存の開発コストと信頼性の限界**: 当時（および現在も）プログラマが正しさを確信する手段は特定ケースの試行（テスト）と修正に限られており、プロジェクト全体の時間・コストの半分以上（機械時間コストを含めると3分の2以上）がデバッグに費やされていた。また稼働後のバグ修正コストや、人命・社会インフラに関わる壊滅的障害のリスクが増大していた。 ## 提案手法 ### 1. 計算機算術の公理化 (Computer Arithmetic) 整数演算の基本的な性質として、以下の公理群（表I）を提示する。これらの公理は非負整数の有限集合上でも成立する。 #### 表I: 整数演算の基本公理 (Table I) | 公理番号 | 公理の内容 | 意味・性質 | | :--- | :--- | :--- | | A1 | $x + y = y + x$ | 加法の交換法則 (addition is commutative) | | A2 | $x \\times y = y \\times x$ | 乗法の交換法則 (multiplication is commutative) | | A3 | $(x + y) + z = x + (y + z)$ | 加法の結合法則 (addition is associative) | | A4 | $(x \\times y) \\times z = x \\times (y \\times z)$ | 乗法の結合法則 (multiplication is associative) | | A5 | $x \\times (y + z) = x \\times y + x \\times z$ | 乗法の加法に対する分配法則 (multiplication distributes through addition) | | A6 | $y \\le x \\supset (x - y) + y = x$ | 加法による減法の打消し (addition cancels subtraction) | | A7 | $x + 0 = x$ | 加法単位元 | | A8 | $x \\times 0 = 0$ | 零の乗法 | | A9 | $x \\times 1 = x$ | 乗法単位元 | 有限集合における最大値を $\\text{max}$ とするとき、無限算術と有限算術は以下の追加公理で区別される: - 無限算術: $\\text{A10}_I \\quad \\neg \\exists x \\forall y \\; (y \\le x)$ - 有限算術: $\\text{A10}_F \\quad \\forall x \\; (x \\le \\text{max})$ さらに、オーバーフロー（$\\text{max} + 1$ の値）に関する3つの扱い（表II）を相互排他な公理として区別できる: - 厳密解釈 (Strict Interpretation): $\\text{A11}_S \\quad \\neg \\exists x \\; (x = \\text{max} + 1)$（オーバーフロー時は結果が存在せずプログラムが完了しない） - 飽和境界 (Firm Boundary): $\\text{A11}_B \\quad \\text{max} + 1 = \\text{max}$（最大値にとどまる） - 剰余算術 (Modulo Arithmetic): $\\text{A11}_M \\quad \\text{max} + 1 = 0$（集合サイズによる剰余） #### 表II: オーバーフロー処理のモデル例（0, 1, 2, 3 の世界） (Table II) 1. 厳密解釈（* は存在しないことを示す）: - 加法: $1+3=*, \\; 2+2=*, \\; 2+3=*, \\; 3+1=*, \\; 3+2=*, \\; 3+3=*$ - 乗法: $1\\times 3=3, \\; 2\\times 2=*, \\; 2\\times 3=*, \\; 3\\times 2=*, \\; 3\\times 3=*$ 2. 飽和境界（最大値 3 に張り付く）: - 加法: $1+3=3, \\; 2+2=3, \\; 2+3=3, \\; 3+1=3, \\; 3+2=3, \\; 3+3=3$ - 乗法: $2\\times 2=3, \\; 2\\times 3=3, \\; 3\\times 2=3, \\; 3\\times 3=3$ 3. 剰余算術（4 を法とする加法・乗法）: - 加法: $1+3=0, \\; 2+2=0, \\; 2+3=1, \\; 3+1=0, \\; 3+2=1, \\; 3+3=2$ - 乗法: $2\\times 2=0, \\; 2\\times 3=2, \\; 3\\times 2=2, \\; 3\\times 3=1$ ### 2. プログラム実行の公理と推論規則 プログラムの実行結果を事前条件 $P$、プログラム $Q$、事後条件 $R$ の三つ組で表現する記法を導入する: $P\\{Q\\}R$ これは「プログラム $Q$ の開始前に表明 $P$ が真であるならば、$Q$ の完了時に表明 $R$ が真となる」と解釈される。前提条件がない場合は $\\text{true}\\{Q\\}R$ と書く。体系内で証明された定理は $\\vdash P\\{Q\\}R$ と表す。 #### D0: 代入公理スキーマ (Axiom of Assignment) 代入文 $x := f$（$x$ は単純変数、$f$ は副作用のない式）に対して: $\\vdash P_0 \\{x := f\\} P$ ここで $P_0$ は表明 $P$ の中のすべての $x$ の出現を $f$ で置換したものである。 #### D1: 帰結規則 (Rules of Consequence) - $\\vdash P\\{Q\\}R$ かつ $\\vdash R \\supset S$ ならば $\\vdash P\\{Q\\}S$ - $\\vdash P\\{Q\\}R$ かつ $\\vdash S \\supset P$ ならば $\\vdash S\\{Q\\}R$ #### D2: 合成規則 (Rule of Composition) 逐次実行 $(Q_1 ; Q_2)$ に対して: $\\vdash P\\{Q_1\\}R_1 \\text{ かつ } \\vdash R_1\\{Q_2\\}R \\implies \\vdash P\\{(Q_1 ; Q_2)\\}R$ #### D3: 反復規則 (Rule of Iteration) ALGOL 60 の $\\text{while } B \\text{ do } S$ 文に対して: $\\vdash P \\land B \\{S\\} P \\implies \\vdash P \\{\\text{while } B \\text{ do } S\\} \\neg B \\land P$ ここで $P$ はループ不変条件（loop invariant）である。 ### 3. 具体例と形式的証明 (Table III) 商 $q$ と余り $r$ を求める逐次減算プログラム: $Q = ((r := x; \\; q := 0); \\; \\text{while } y \\le r \\text{ do } (r := r - y; \\; q := 1 + q))$ 証明すべき仕様定理: $\\text{true}\\{Q\\} \\neg (y \\le r) \\land x = r + y \\times q$ #### 表III: 形式的証明の手順 (Table III) | 行番号 | 形式的証明の論理式 | 正当化の根拠 (Justification) | | :--- | :--- | :--- | | 1 | $\\text{true} \\supset x = x + y \\times 0$ | 補題1（公理 A7, A8 より） | | 2 | $x = x + y \\times 0 \\;\\{r := x\\}\\; x = r + y \\times 0$ | D0（代入公理） | | 3 | $x = r + y \\times 0 \\;\\{q := 0\\}\\; x = r + y \\times q$ | D0（代入公理） | | 4 | $\\text{true} \\;\\{r := x\\}\\; x = r + y \\times 0$ | D1 (1, 2)（帰結規則） | | 5 | $\\text{true} \\;\\{r := x; \\; q := 0\\}\\; x = r + y \\times q$ | D2 (4, 3)（合成規則） | | 6 | $x = r + y \\times q \\land y \\le r \\supset x = (r - y) + y \\times (1 + q)$ | 補題2（公理 A3, A5, A6, A9 より） | | 7 | $x = (r - y) + y \\times (1 + q) \\;\\{r := r - y\\}\\; x = r + y \\times (1 + q)$ | D0（代入公理） | | 8 | $x = r + y \\times (1 + q) \\;\\{q := 1 + q\\}\\; x = r + y \\times q$ | D0（代入公理） | | 9 | $x = (r - y) + y \\times (1 + q) \\;\\{r := r - y; \\; q := 1 + q\\}\\; x = r + y \\times q$ | D2 (7, 8)（合成規則） | | 10 | $x = r + y \\times q \\land y \\le r \\;\\{r := r - y; \\; q := 1 + q\\}\\; x = r + y \\times q$ | D1 (6, 9)（帰結規則） | | 11 | $x = r + y \\times q \\;\\{\\text{while } y \\le r \\text{ do } (r := r - y; \\; q := 1 + q)\\}\\; \\neg(y \\le r) \\land x = r + y \\times q$ | D3 (10)（反復規則） | | 12 | $\\text{true} \\;\\{((r := x; \\; q := 0); \\; \\text{while } y \\le r \\text{ do } (r := r - y; \\; q := 1 + q))\\}\\; \\neg(y \\le r) \\land x = r + y \\times q$ | D2 (5, 11)（合成規則） | ## 新規性 - **プログラム構文に基づく公理的体系化**: Floyd (1967) の表明法はフローチャート（グラフ構造）を対象としていたのに対し、Hoare はプログラミング言語のテキスト構文（代入文、逐次合成、while文）に直接適用可能な推論規則を構築した。 - **逆方向置換による代入公理の発見**: 代入文 $x := f$ の意味を「代入後の $P(x)$ を保証するには代入前に $P(f)$ が成り立っていなければならない」という直感的に極めて明快かつ論理的に厳密な置換規則（公理スキーマ D0）として定式化した。 - **部分正当性記法（ホーアの三つ組）の確立**: 事前条件・プログラム・事後条件を一体として記述する記法 $P\\{Q\\}R$ を世界で初めて導入した。 ## 考察 ### 適用限界と保留事項 (General Reservations) 1. **副作用の不在仮定**: 式や条件の評価における副作用（side effects）がないことを前提としている。副作用を許す言語では、証明技法を適用する前に副作用の不在を個別に証明する必要があり、高水準言語において副作用を伴う手続き関数呼び出しを用いることの実質的な利点に疑問を呈している。 2. **部分正当性（Partial Correctness）の限界**: $P\\{Q\\}R$ は「プログラムが正常に停止するならば、結果は $R$ を満たす」という条件付き正当性（conditional correctness / partial correctness）を述べるに過ぎず、停止性の証明は提供しない。停止失敗の原因には無限ループだけでなく、実装依存の制限違反（オーバーフロー、記憶容量超過、OS制限時間超過）が含まれる。 3. **未カバーの言語機能**: 実数演算、ビット・文字操作、配列、レコード、ファイル、入出力、宣言、サブルーチン、パラメータ、再帰、並列実行は本論文では扱われていない。特に**ラベルとジャンプ（goto）**、**ポインタ**、**名前渡しパラメータ**は公理的扱いが本質的に困難であり、下底の公理の複雑化を招くと指摘している。 ### 形式的言語定義への影響 公理的意味論は、ALGOL 60 の BNF が構文定義に果たした役割と同様の明晰さを意味論にもたらす。さらに、言語仕様ですべてを過剰に決定せず、オーバーフロー処理や浮動小数点の精度などの実装依存部分を選択可能な追加公理として「未定義のまま残す」柔軟な枠組みを提供する。 ## 強み / 弱点・課題 ### 強み - **直感性と論理的厳密性の両立**: プログラミング言語の意味を数理論理学の一階述語論理の中に直接位置づけ、人間および機械検証器による形式的演繹を可能にした。 - **モジュラーな推論**: 合成規則やサブルーチンの補題化により、プログラム全体の構造と証明の構造が一致する。 - **言語設計へのフィードバック**: 「証明しやすい言語機能が良い言語機能である」という指針を与え、副作用や複雑なポインタ・ジャンプを制限する構造化プログラミングの理論的支柱となった。 ### 弱点・課題 - **停止性の未保証**: 停止性証明（全正当性 / total correctness）には別途整列集合上の導出変数の導入などが必要。 - **実用的言語機能の困難さ**: ポインタ、エイリアシング、例外、並列性、ジャンプ文が存在する場合、公理系が著しく複雑化する。 - **手作業の形式証明の労力**: 論文自身が認めている通り、完全な形式的証明は「過度に退屈（excessively tedious）」であり、補題やメタ規則による証明の省略や自動証明器の支援が不可欠である。 ## 関連 - 概念: [[公理的意味論]]、[[不変条件]]、[[形式手法]] - 人物: [[C. A. R. Hoare]]、[[Robert W. Floyd]] - 組織: [[Queen's University Belfast]] ## 出典 - C. A. R. Hoare, "An Axiomatic Basis for Computer Programming", *Communications of the ACM*, Vol. 12, No. 10, pp. 576–580, 583, October 1969.