公理的意味論
公理的意味論（Axiomatic Semantics）は、プログラムの意味を論理的な命題として捉え、プログラムの正しさや性質を形式的に証明するための方法です。プログラムの動作そのものを直接表現するのではなく、プログラムの実行前後の状態に関する論理的な性質（前提条件と後述条件）に基づいて、プログラムが期待通りに動作するかどうかを確認します。 公理的意味論の基礎は、C.A.R. Hoareによって提唱されたホーア論理にあります。ホーア論理は、プログラムの正しさを形式的に証明するためのフレームワークであり、以下の要素から成り立ちます。
ホーア三つ組（Hoare Triple）
$ \{P\} \; C \; \{Q\}
P（前提条件）: プログラム (C) の実行前に成立しているべき条件。
C（コマンド）: プログラムの命令やステートメント。
Q（後述条件）: プログラム (C) の実行後に成立しているべき条件。
このホーア三つ組は、「もし前提条件 (P) が成立しているならば、プログラム (C) を実行した後には後述条件 (Q) が成立している」という意味を表します。