Hoareの章におけるホーア論理の提示を「モデル理論的」("model-theoretic")に行うこともできたでしょう。 それぞれのコンストラクタに対する証明規則をプログラムの振舞いについての「定理」として提示し、プログラムの正しさ（ホーアの三つ組の正しさ）の証明は、 それらの定理をCoq内で直接組み合わせることで構成するのです。 ホーア論理を提示するもう一つの方法は、完全に別個の証明体系を定義することです。 コマンドやホーアの三つ組等についての公理と推論規則の集合を定めます。 ホーアの三つ組の証明とは、定義されたこの論理で正しく導出されたもののことになります。 こうするためには、新しい論理で正しい導出(valid derivations)の帰納的定義を与えれば良いのです。 この章はオプションです。 先に「論理の基礎」（「ソフトウェアの基礎」の第一巻）のProofObjectsの章を読んだ方がいいかもしれません。

定義

We don't need to include axioms corresponding to hoare_consequence_pre or hoare_consequence_post, because these can be proven easily from H_Consequence.

例として、ホーアの三つ組
      {{(X=3) [X |-> X + 2] [X |-> X + 1]}}
      X::=X+1 ;; X::=X+2
      {{X=3}}

の導出を表現する証明オブジェクトを構成しましょう。 証明オブジェクトを構成するのに Coq のタクティックを使うことができます。

性質

練習問題: ★★, standard (hoare_proof_sound)

これらの証明オブジェクトが真の主張を表現することを証明しなさい。

☐

Coqの推論機構をホーア論理についてのメタ定理を証明することに使うこともできます。 例えば、Hoareで見た2つの定理に対応するものを以下に示します。 ここではホーアの三つ組の意味論から直接にではなく、ホーア論理の導出（証明可能性）の構文の面から表現します。 最初のものは、すべてのPとcについて、表明{{P}} c {{True}}がホーア論理で証明可能(provable)であることを言うものです。 Hoareにおける意味論的証明と比べて、この証明はより複雑になることに注意して下さい。 実際、コマンドcの構造についての帰納法を行う必要があります。

同様に、任意のcとQについて{{False}} c {{Q}}が証明可能であることを示すことができます。

As a last step, we can show that the set of hoare_proof axioms is sufficient to prove any true fact about (partial) correctness. More precisely, any semantic Hoare triple that we can prove can also be proved from these axioms. Such a set of axioms is said to be relatively complete. Our proof is inspired by this one: http://www.ps.uni-saarland.de/courses/sem-ws11/script/Hoare.html To carry out the proof, we need to invent some intermediate assertions using a technical device known as weakest preconditions. Given a command c and a desired postcondition assertion Q, the weakest precondition wp c Q is an assertion P such that {{P}} c {{Q}} holds, and moreover, for any other assertion P', if {{P'}} c {{Q}} holds then P' -> P. We can more directly define this as follows:

Exercise: 1 star, standard (wp_is_precondition)

☐

Exercise: 1 star, standard (wp_is_weakest)

The following utility lemma will also be useful.

☐

Exercise: 5 stars, standard (hoare_proof_complete)

Complete the proof of the theorem.

☐

最後に、この公理的ホーア論理が「決定可能(decidable)」であればとても喜ばしいでしょう。 つまり、ある（終了する）アルゴリズム（決定手続き(decision procedure)）が、ホーアの三つ組が妥当（導出可能）かを判定してくれると嬉しいでしょう。 しかしそんな決定手続きは存在しないのです！ {{True}} c {{False}} という三つ組を考えてみましょう。 この三つ組は、cが終了しないとき、かつそのときに限り妥当です。 つまり、これが妥当かを判定するアルゴリズムは、停止性問題を解いてしまうのです。 同様に、任意のCoqの論理における言明 P に対して、三つ組 {{True} SKIP {{P}} は forall s, P s が妥当であるとき、かつそのときに限り妥当です。 しかし、そのような決定手続きがないことも知られています。 全体として、この表現の公理的形式は「ホーア論理の証明を与えること」がどういう意味なのかについて、より明確なイメージを与えてくれます。 しかし、実際の証明を記述するという観点からは完全に満足できるものではありません。 かなりくどいのです。 Hoare2の修飾付きプログラムの形式化の節が、より良い方法を示してくれます。