# 公理的意味論 ## 定義 公理的意味論（axiomatic semantics）とは、プログラミング言語の構文要素の意味を、その実行前後で成立すべき論理的表明（assertion）の関係を規定する公理と推論規則の体系として定義する手法である。C. A. R. Hoare（1969）が Robert W. Floyd（1967）のフローチャート上の表明法をテキスト構文へと発展させて提唱し、その論理体系は**ホーア論理（Hoare logic）**と呼ばれる。基本要素は事前条件 $P$、プログラム文 $Q$、事後条件 $R$ からなる**ホーアの三つ組（Hoare triple）** $P\{Q\}R$ であり、「実行前に $P$ が成り立つならば、プログラム $Q$ が停止したとき実行後に $R$ が成り立つ」という部分正当性（partial correctness）を記述する。代入文の公理スキーマ $P_0\{x := f\}P$ や合成・反復・帰結の規則により、プログラムの数学的仕様を純粋な演繹的推論によって証明できる。(Source: [[@1969__CACM__An Axiomatic Basis for Computer Programming]]) ## 未解決の問い - ポインタやヒープの動的割り当て（エイリアシング）が存在する言語機能に対して、古典的ホーア論理の代入公理（単純なテキスト置換）をどのように拡張・一般化できるか（分離論理 / Separation Logic 等との接続）。 - ホーア論理による部分正当性の証明と、整列集合を用いた停止性証明（全正当性）を統一的に扱う検証系において、証明義務の自動生成と解決はどこまで自動化可能か。 - 手続き呼び出しや再帰、並列実行を含む高水準言語に対して、公理的意味論はどの程度の複雑性で一貫した体系を提供できるか。 ## 未編纂の観察 - ## 関連 - ソース: [[@1969__CACM__An Axiomatic Basis for Computer Programming]] - 概念: [[形式手法]]、[[不変条件]] - 人物: [[C. A. R. Hoare]]、[[Robert W. Floyd]] ## 出典 - C. A. R. Hoare, "An Axiomatic Basis for Computer Programming", *Communications of the ACM*, 1969.