「論理の基礎」（「ソフトウェアの基礎」第一巻）の最後の章では、コースの最初に用意した数学的道具を、小さなプログラミング言語 Imp の理論の学習に適用してみました。

• Imp の抽象構文木(abstract syntax trees)の型を定義しました。 また、操作的意味論(operational semantics)を与える評価関係(evaluation relation)（状態間の部分関数）も定義しました。
  定義した言語は小さいですが、C, C++, Java などの本格的な言語の主要な機能を持っています。 その中には変更可能な状態や、いくつかのよく知られた制御構造も含まれます。
• いくつものメタ理論的性質(metatheoretic properties)を証明しました。 "メタ"というのは、言語で書かれた特定のプログラムの性質ではなく言語自体の性質という意味です。 証明したものには、以下のものが含まれます:
  • 評価の決定性
  • 異なった書き方をした定義の同値性（例：算術式の関数による評価と関係による評価）
  • プログラムのあるクラスの、停止性の保証
  • いくつかの有用なプログラム変換の正当性（意味の保存）
  • プログラムの動作の同値性（Equivの章において）

もしここで止めたとしても、有用なものを持っていることになります。 それは、プログラミング言語とその特性を定義し議論する、数学的に正確で、柔軟で、使いやすい、主要な性質に適合した道具です。 これらの性質は、言語を設計する人、コンパイラを書く人、そしてユーザも知っておくべきものです。 実際、その多くは我々が扱うプログラミング言語を理解する上で本当に基本的なことですので、「定理」と意識することはなかったかもしれません。 しかし、直観的に明らかだと思っている性質はしばしばとても曖昧で、時には間違っていることもあります! 言語に対するメタな性質については、この巻の後ろで型(types)とその健全性(type soundness)を議論する際に再度出てきます。 この章では、別の問題について進めます。 本章のゴールは、「プログラム検証(program verification)」をいくつか行うことです。 そのために、Imp言語の特定のプログラムがある性質を満たすかについて、形式的に証明するための適切な定義を用います。 一般にフロイド-ホーア論理(Floyd-Hoare Logic)、あるいは、単にホーア論理(Hoare Logic)と呼ばれる推論システムを作ります。 この推論システムの中では、Imp の各構文要素に対してそれぞれ一般的な「証明規則(proof rule)」が与えられ、プログラムの構造に基づいて正当性を推論できるようになっています。 ホーア論理の起源は1960年代です。 そして今現在まで継続してさかんに研究がされています。 実際のソフトウェアシステムの仕様を定め検証するために使われている非常に多くのツールは、ホーア論理を核としているのです。 ホーア論理は2つの重要なことがらを提供します。プログラムの仕様(specification)を自然に記述する方法と、その仕様が適合していることを証明する合成的証明法(compositional proof technique)です。 ここでの「合成的(compositional)」という意味は、証明の構造が証明対象となるプログラムの構造を直接的に反映しているということです。 Overview of this chapter... Topic:

• A systematic method for reasoning about the functional correctness of programs in Imp

Goals:

• a natural notation for program specifications and
• a compositional proof technique for program correctness

Plan:

• specifications (assertions / Hoare triples)
• proof rules
• loop invariants
• decorated programs
• examples

表明

プログラムの仕様について話そうとするとき、最初に欲しくなるのは、実行中のある特定の時点で成立している性質 つまり、プログラム実行時にその箇所に来た時の状態に関して成り立つ言明 -- についての表明(assertions)を作る方法です。 形式的には、表明は状態に関する述語です。

練習問題: ★, standard, optional (assertions)

以下の表明を日本語（または好きな自然言語）に直しなさい。

☐

この方法で表明を書くことは、2つの理由から、若干ヘビーに見えます。 (1)すべての個々の表明は、fun st => から始まっています。 (2)状態stは表明から変数を参照するために使う唯一の状態です（2つの別々の状態を同時に考える必要はありません）。 例について非形式的に議論するときには、いくらか簡単にします。 最初のfun st =>は書かず、st Xのかわりに単にXと書きます。 つまり、非形式的には、次のように書くかわりに
      fun st => (st Z) * (st Z) <= m /\
                ~ ((S (st Z)) * (S (st Z)) <= m)

次のように書きます。
      Z * Z <= m /\ ~((S Z) * (S Z) <= m)

この例は、ホーア論理の章を通じて使う慣習に則っています。 非形式的な表明では、X、Y、Zのような大文字の変数をImpの変数とし、x、y、m、nなどの小文字の変数をCoqの（nat型の）変数とします。 そのため、この非形式的な表明を形式的な表明に変換する際には、Xをst Xに置き換えますが、mはそのままにします。 Given two assertions P and Q, we say that P implies Q, written P ->> Q, if, whenever P holds in some state st, Q also holds.

このhoare_spec_scopeアノテーションは、Coqに、この記法はグローバルではなく特定のコンテキストで使うものであることを伝えるものです。 Open Scopeは、このファイルがそのコンテキストであることを Coq に伝えます。 We'll also want the "iff" variant of implication between assertions:

ホーアの三つ組

次に、コマンドの振舞いについての形式的表明を作る方法が必要です。

一般に、コマンドの振舞いは、状態を別の状態に変換するものです。 そのため、コマンドについて言及するには、コマンドの実行前と後の状態で真になる表明を用いるのが自然でしょう。

• 「もし c が表明 P を満たす状態から開始され、また、cがいつかは停止するならば、最終状態では、表明Qが成立する。」

このような言明は ホーアの三つ組(Hoare Triple)と呼ばれます。 表明Pはcの事前条件(precondition)と呼ばれます。 Qはcの事後条件(postcondition)と呼ばれます。

形式的には以下の通りです。

ホーアの三つ組を今後多用するので、簡潔な記法を用意すると便利です:
       {{P}} c {{Q}}

（伝統的には、ホーアの三つ組は {P} c {Q}と書かれます。 しかし Coq では一重の波カッコは別の意味で既に使われています。）

練習問題: ★, standard, optional (triples)

以下のホーアの三つ組を日本語に直しなさい。
   1) {{True}} c {{X = 5}}
 
   2) {{X = m}} c {{X = m + 5}}
 
   3) {{X <= Y}} c {{Y <= X}}
 
   4) {{True}} c {{False}}
 
   5) {{X = m}}
      c
      {{Y = real_fact m}}
 
   6) {{X = m}}
      c
      {{(Z * Z) <= m /\ ~ (((S Z) * (S Z)) <= m)}}

練習問題: ★, standard, optional (valid_triples)

以下のホーアの三つ組のうち、正しい(valid)ものを選択しなさい。 正しいとは、P,c,Qの関係が真であるということです。
   1) {{True}} X ::= 5 {{X = 5}}
 
   2) {{X = 2}} X ::= X + 1 {{X = 3}}
 
   3) {{True}} X ::= 5;; Y ::= 0 {{X = 5}}
 
   4) {{X = 2 /\ X = 3}} X ::= 5 {{X = 0}}
 
   5) {{True}} SKIP {{False}}
 
   6) {{False}} SKIP {{True}}
 
   7) {{True}} WHILE true DO SKIP END {{False}}
 
   8) {{X = 0}}
        WHILE X = 0 DO X ::= X + 1 END
      {{X = 1}}
 
   9) {{X = 1}}
        WHILE ~(X = 0) DO X ::= X + 1 END
      {{X = 100}}

ウォーミングアップとして、ホーアの三つ組についての2つの事実を見てみます。 （何を意味しているのかしっかり理解してください。）

証明規則

ホーア論理のゴールは、特定のホーアの三つ組の正しさを証明する"合成的"手法を提供することです。 つまり、プログラムの正しさの証明の構造を、プログラムの構造を反映させたものにしたいということです。 このために、以降の節では、Impのコマンドの構文要素それぞれに対して、推論するための規則を1つずつ導入します。 つまり、代入に1つ、コマンド合成に1つ、条件分岐に1つ、等です。 それに加えて、複数のものを結合するために有用な2つの"構造的"規則を導入します。 これらの規則を用いて、hoare_tripleの定義を展開することなしにプログラムの正しさを証明していきます。

代入

代入の規則は、ホーア論理の証明規則の中で最も基本的なものです。 この規則は次のように働きます。 次の正しいホーアの三つ組を考えます。
       {{ Y = 1 }} X ::= Y {{ X = 1 }}

日本語で言うと、Yの値が1である状態から始めて、XにYを代入すれば、Xが1である状態になる、ということです。 つまり、1である、という性質がYからXに移された、ということです。

同様に、
       {{ Y + Z = 1 }} X ::= Y + Z {{ X = 1 }}

においては、同じ性質（1であること）が代入の右辺のY + ZからXに移動されています。

より一般に、aが「任意の」算術式のとき、
       {{ a = 1 }} X ::= a {{ X = 1 }}

は正しいホーアの三つ組になります。

さらに一般化して、任意の性質QがX ::= aの後に成り立つには、X ::= aの前で、Q内の「出現している全ての」Xをaに置き換えたものが成り立っている必要があります。 ここから次の、代入に関するホーアの三つ組が導かれます。
      {{ Q [X |-> a] }} X ::= a {{ Q }}

ただし、"Q [X |-> a]"は「Xをaに置換したQ」と読みます。

例えば、以下は、代入規則の正しい適用です:
      {{ (X <= 5) [X |-> X + 1]
         i.e., X + 1 <= 5 }}
      X ::= X + 1
      {{ X <= 5 }}
 
      {{ (X = 3) [X |-> 3]
         i.e., 3 = 3 }}
      X ::= 3
      {{ X = 3 }}
 
      {{ (0 <= X /\ X <= 5) [X |-> 3]
         i.e., (0 <= 3 /\ 3 <= 5) }}
      X ::= 3
      {{ 0 <= X /\ X <= 5 }}

To formalize the rule, we must first formalize the idea of "substituting an expression for an Imp variable in an assertion", which we refer to as assertion substitution, or assn_sub. That is, given a proposition P, a variable X, and an arithmetic expression a, we want to derive another proposition P' that is just the same as P except that P' should mention a wherever P mentions X. Since P is an arbitrary Coq assertion, we can't directly "edit" its text. However, we can achieve the same effect by evaluating P in an updated state:

That is, P [X |-> a] stands for an assertion -- let's call it P' -- that is just like P except that, wherever P looks up the variable X in the current state, P' instead uses the value of the expression a. To see how this works, let's calculate what happens with a couple of examples. First, suppose P' is (X <= 5) [X |-> 3] -- that is, more formally, P' is the Coq expression fun st => (fun st' => st' X <= 5) (X !-> aeval st 3 ; st), which simplifies to fun st => (fun st' => st' X <= 5) (X !-> 3 ; st) and further simplifies to fun st => ((X !-> 3 ; st) X) <= 5 and finally to fun st => 3 <= 5. That is, P' is the assertion that 3 is less than or equal to 5 (as expected). For a more interesting example, suppose P' is (X <= 5) [X |-> X + 1]. Formally, P' is the Coq expression fun st => (fun st' => st' X <= 5) (X !-> aeval st (X + 1) ; st), which simplifies to fun st => (X !-> aeval st (X + 1) ; st) X <= 5 and further simplifies to fun st => (aeval st (X + 1)) <= 5. That is, P' is the assertion that X + 1 is at most 5.

置換を用いることで、正確な代入の証明規則を与えます:
      ------------------------------ (hoare_asgn)
      {{Q [X |-> a]}} X ::= a {{Q}}

We can prove formally that this rule is indeed valid.

この規則を使った最初の形式的証明が次のものです。

Of course, what would be even more helpful is to prove this simpler triple: X < 4 X ::= X + 1 X < 5 We will see how to do so in the next section.

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

次の非形式的なホーアの三つ組...
    1) {{ (X <= 10) [X |-> 2 * X] }}
       X ::= 2 * X
       {{ X <= 10 }}
 
    2) {{ (0 <= X /\ X <= 5) [X |-> 3] }}
       X ::= 3
       {{ 0 <= X /\ X <= 5 }}

...を、形式的記述に直し（それぞれの名前をassn_sub_ex1、assn_sub_ex2とする）、hoare_asgnを使って証明しなさい。

☐

練習問題: ★★, standard, recommended (hoare_asgn_wrong)

代入規則は、最初に見たとき、ほとんどの人が後向きの規則であるように感じます。 もし今でもパズルのように見えるならば、「前向き」バージョンの規則を考えてみるのも良いでしょう。 次のものは自然に見えます:
      ------------------------------ (hoare_asgn_wrong)
      {{ True }} X ::= a {{ X = a }}

この規則が正しくないことを示す反例を挙げ、それが実際に反例となっていることを非形式的に示しなさい。 （ヒント：この規則は算術式aを量化しているので、反例はこの規則がうまく動かないようにaを提示する必要があります。）

☐

Exercise: 3 stars, advanced (hoare_asgn_fwd)

However, by using a parameter m (a Coq number) to remember the original value of X we can define a Hoare rule for assignment that does, intuitively, "work forwards" rather than backwards.

---

(hoare_asgn_fwd) fun st => P st /\ st X = m X ::= a fun st => P st' /\ st X = aeval st' a (where st' = (X !-> m ; st)) Note that we use the original value of X to reconstruct the state st' before the assignment took place. Prove that this rule is correct. (Also note that this rule is more complicated than hoare_asgn.)

☐

Exercise: 2 stars, advanced, optional (hoare_asgn_fwd_exists)

Another way to define a forward rule for assignment is to existentially quantify over the previous value of the assigned variable. Prove that it is correct.

---

(hoare_asgn_fwd_exists) fun st => P st X ::= a fun st => exists m, P (X !-> m ; st) /\ st X = aeval (X !-> m ; st) a

☐

帰結

ホーア規則から得られる事前条件や事後条件が欲しいものと完全には一致しない、ということが身近な場面においてしばしば起こります。 それらは論理的には証明しようとするゴールと同値にも関わらず、構文上違う形をしているために単一化できない、という場合がありえます。 あるいは、想定するゴールに比べて、（事前条件について）論理的に弱かったり、（事後条件について）論理的に強かったりすることがあります。 例えば、
      {{(X = 3) [X |-> 3]}} X ::= 3 {{X = 3}}

が代入規則に直接従うのに対して、より自然な三つ組
      {{True}} X ::= 3 {{X = 3}}

はそうではないのです。 この三つ組も正しいのですが、hoare_asgn のインスタンスではないのです。 なぜなら、True と (X = 3) [X |-> 3] は、構文的に等しい表明ではないからです。 しかし、これらが論理的に「等価」である以上、一方の三つ組が正しいのであれば、もう一方も同様に正しくあるべきです。 このことを、以下の規則によって表現します。
                {{P'}} c {{Q}}
                  P <<->> P'
         ----------------------------- (hoare_consequence_pre_equiv)
                {{P}} c {{Q}}

これを進めていくと、ある正しい三つ組から別の記述による正しい三つ組を生成する、事前条件の弱化と事後条件の強化が出てきます。 これは以下の「帰結に関する規則」に集約されます。
                {{P'}} c {{Q}}
                   P ->> P'
         ----------------------------- (hoare_consequence_pre)
                {{P}} c {{Q}}
 
                {{P}} c {{Q'}}
                  Q' ->> Q
         ----------------------------- (hoare_consequence_post)
                {{P}} c {{Q}}

以下が形式化版です:

例えば、一つ目の帰結規則を次のように使うことができます:
      {{ True }} ->>
      {{ 1 = 1 }}
    X ::= 1
      {{ X = 1 }}

あるいは、形式化すると...

We can also use it to prove the example mentioned earlier. X < 4 ->> (X < 5)[X |-> X + 1] X ::= X + 1 X < 5 Or, formally ...

Finally, for convenience in proofs, here is a combined rule of consequence that allows us to vary both the precondition and the postcondition in one go. P' c Q' P ->> P' Q' ->> Q

---

(hoare_consequence) P c Q

余談: eapply タクティック

良い機会ですので、「論理の基礎」の Auto 章で概要を説明した eapply を別の観点から説明しましょう。 上述の hoare_asgn_example1 や hoare_consequence の証明では、 hoare_consequence_pre 規則のメタ変数を明示するために、with (P' := ...) のように書かなければいけませんでした。 （というのも、hoare_consequence_pre の P' は帰結に出ないので、帰結と現在のゴールを単一化しても P' を特定することはできません。） これは少し鬱陶しいです。 というのも、それなりに長くなりますし、また hoare_asgn_example1 では、直後に行う hoare_asgn 規則の適用がそこに入る表明を明らかにするからです。 このような場合に、apply の代わりに eapply を使えます。 これは基本的に「少し我慢してください、抜けている部分は後で埋めます」と Coq に伝えることに相当します。

In general, the eapply H tactic works just like apply H except that, instead of failing if unifying the goal with the conclusion of H does not determine how to instantiate all of the variables appearing in the premises of H, eapply H will replace these variables with existential variables (written ?nnn), which function as placeholders for expressions that will be determined (by further unification) later in the proof. In order for Qed to succeed, all existential variables need to be determined by the end of the proof. Otherwise Coq will (rightly) refuse to accept the proof. Remember that the Coq tactics build proof objects, and proof objects containing existential variables are not complete.

Coq gives a warning after apply HP. ("All the remaining goals are on the shelf," means that we've finished all our top-level proof obligations but along the way we've put some aside to be done later, and we have not finished those.) Trying to close the proof with Qed gives an error.

An additional constraint is that existential variables cannot be instantiated with terms containing ordinary variables that did not exist at the time the existential variable was created. (The reason for this technical restriction is that allowing such instantiation would lead to inconsistency of Coq's logic.)

Doing apply HP' above fails with the following error: Error: Impossible to unify "?175" with "y". In this case there is an easy fix: doing destruct HP before doing eapply HQ.

The apply HP' in the last step unifies the existential variable in the goal with the variable y. Note that the assumption tactic doesn't work in this case, since it cannot handle existential variables. However, Coq also provides an eassumption tactic that solves the goal if one of the premises matches the goal up to instantiations of existential variables. We can use it instead of apply HP' if we like.

Exercise: 2 stars, standard (hoare_asgn_examples_2)

Translate these informal Hoare triples... X + 1 <= 5 X ::= X + 1 X <= 5 0 <= 3 /\ 3 <= 5 X ::= 3 0 <= X /\ X <= 5 ...into formal statements (name them assn_sub_ex1' and assn_sub_ex2') and use hoare_asgn and hoare_consequence_pre to prove them.

☐

Skip

SKIPは状態を変えないことから、任意の表明 P を保存します:
      -------------------- (hoare_skip)
      {{ P }} SKIP {{ P }}

コマンド合成

より興味深いことに、コマンドc1がPが成立する任意の状態をQが成立する状態にし、c2がQが成立する任意の状態をRが成立する状態にするとき、 c1に続いてc2を行うことは、Pが成立する任意の状態をRが成立する状態にします:
        {{ P }} c1 {{ Q }}
        {{ Q }} c2 {{ R }}
       ---------------------- (hoare_seq)
       {{ P }} c1;c2 {{ R }}

形式的規則hoare_seqにおいては、前提部分が「逆順」である（c1の前にc2が来る）ことに注意してください。 この順は、規則を使用する多くの場面で情報の自然な流れにマッチするのです。 ホーア論理における証明の構築はプログラムの終わりから（最後の事後条件を用いて）、プログラムの始めにたどり着くまでコマンドをさかのぼる方が自然なのです。

非形式的には、この規則を利用した証明を表す良い方法は、c1とc2の間に中間表明Qを記述する"修飾付きプログラム"の様にすることです:
      {{ a = n }}
    X ::= a;;
      {{ X = n }} <--- 修飾 Q
    SKIP
      {{ X = n }}

Here's an example of a program involving both assignment and sequencing.

We typically use hoare_seq in conjunction with hoare_consequence_pre and the eapply tactic, as in this example.

練習問題: ★★, standard, recommended (hoare_asgn_example4)

次の修飾付きプログラムを形式的証明に直しなさい:
                   {{ True }} ->>
                   {{ 1 = 1 }}
    X ::= 1;;
                   {{ X = 1 }} ->>
                   {{ X = 1 /\ 2 = 2 }}
    Y ::= 2
                   {{ X = 1 /\ Y = 2 }}

（"->>"という記法はhoare_consequence_preを使ったことを示しています。）

☐

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

XとYの値を交換するImpプログラムcを書き、それが次の仕様を満たすことを示しなさい:
      {{X <= Y}} c {{Y <= X}}

証明にunfold hoare_tripleを使わないようにすること。 （ヒント：代入の規則は「後ろから前」、つまり事後条件から事前条件に向かって用いることを覚えておいてください。 結果的にプログラムの後ろから前に向かって証明することになるでしょう。）

☐

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

次の命題が証明できない理由を説明しなさい:
      forall (a : aexp) (n : nat),
         {{fun st => aeval st a = n}}
           X ::= 3;; Y ::= a
         {{fun st => st Y = n}}.

☐

条件分岐

条件分岐コマンドについて推論するために、どのような規則が必要でしょうか？ もちろん、分岐のどちらの枝を実行した後でも表明Qが成立するならば、条件分岐全体でもQが成立するでしょう。 これから次のように書くべきかもしれません:
              {{P}} c1 {{Q}}
              {{P}} c2 {{Q}}
      ---------------------------------
      {{P}} TEST b THEN c1 ELSE c2 {{Q}}

しかし、これはかなり弱いのです。 例えば、この規則を使っても次のことを示すことができません:
     {{ True }}
     TEST X = 0
       THEN Y ::= 2
       ELSE Y ::= X + 1
     FI
     {{ X <= Y }}

なぜなら、この規則では、"then"部と"else"部のどちらの代入が起こる状態なのかについて、何も言っていないからです。

実際にはより詳しいことを言うことができます。 "then"部では、ブール式bの評価結果がtrueになることがわかっています。 また"else"部では、それがfalseになることがわかっています。 この情報を補題の前提部分で利用できるようにすることで、c1とc2の振舞いについて（つまり事後条件Qが成立する理由について）推論するときに、より多くの情報を使うことができるようになります。
              {{P /\ b}} c1 {{Q}}
              {{P /\ ~ b}} c2 {{Q}}
      ------------------------------------ (hoare_if)
      {{P}} TEST b THEN c1 ELSE c2 FI {{Q}}

この規則を形式的に解釈するために、もう少しやることがあります。 厳密には、上述の表明において、表明とブール式の連言P /\ bは、型チェックを通りません。 これを修正するために、ブール式bを形式的に「持ち上げ」て、表明にしなければなりません。 このためにbassn bと書きます。 これは"ブール式bの評価結果が（任意の状態で）trueになる"という表明です。

bassnについての2つの便利な事実です:

いよいよ条件分岐についてのホーア証明規則を形式化し、正しいことを証明できます。

例

以下が、最初に挙げたプログラムが与えられた条件を満たすことの証明です。

Exercise: 2 stars, standard (if_minus_plus)

Prove the following hoare triple using hoare_if. Do not use unfold hoare_triple.

☐

Exercise: One-sided conditionals

Exercise: 4 stars, standard (if1_hoare)

In this exercise we consider extending Imp with "one-sided conditionals" of the form IF1 b THEN c FI. Here b is a boolean expression, and c is a command. If b evaluates to true, then command c is evaluated. If b evaluates to false, then IF1 b THEN c FI does nothing. We recommend that you complete this exercise before attempting the ones that follow, as it should help solidify your understanding of the material. The first step is to extend the syntax of commands and introduce the usual notations. (We've done this for you. We use a separate module to prevent polluting the global name space.)

Next we need to extend the evaluation relation to accommodate IF1 branches. This is for you to do... What rule(s) need to be added to ceval to evaluate one-sided conditionals?

Now we repeat (verbatim) the definition and notation of Hoare triples.

Finally, we (i.e., you) need to state and prove a theorem, hoare_if1, that expresses an appropriate Hoare logic proof rule for one-sided conditionals. Try to come up with a rule that is both sound and as precise as possible.

For full credit, prove formally hoare_if1_good that your rule is precise enough to show the following valid Hoare triple: X + Y = Z IF1 ~(Y = 0) THEN X ::= X + Y FI X = Z Hint: Your proof of this triple may need to use the other proof rules also. Because we're working in a separate module, you'll need to copy here the rules you find necessary.

☐

ループ

最後に、ループについての推論規則が必要です。

次のループを考えます:
      WHILE b DO c END

そして、次の三つ組が正しくなる事前条件Pと事後条件Qを探します:
      {{P}} WHILE b DO c END {{Q}}

まず、bが最初から偽であるときを考えましょう。 このときループの本体はまったく実行されません。 この場合は、ループはSKIPと同様の振舞いをしますので、次のように書いても良いかもしれません。

      {{P}} WHILE b DO c END {{P}}

しかし、条件分岐について議論したのと同様に、最後でわかっていることはもう少し多いのです。 最終状態ではPであるだけではなくbが偽になっているのです。 そこで、事後条件にちょっと付け足すことができます:
      {{P}} WHILE b DO c END {{P /\ ~ b}}

それでは、ループの本体が実行されるときはどうなるでしょう？ ループを最後に抜けるときにはPが成立することを確実にするために、コマンドcの終了時点で常にPが成立することを確認する必要があるのは確かでしょう。 さらに、Pがcの最初の実行の前に成立しており、cを実行するたびに、終了時点でPの成立が再度確立されることから、Pがcの実行前に常に成立していると仮定することができます。 このことから次の規則が得られます:
                   {{P}} c {{P}}
        -----------------------------------
        {{P}} WHILE b DO c END {{P /\ ~ b}}

これで求める規則にかなり近付いたのですが、もうちょっとだけ改良できます。 ループ本体の開始時点で、Pが成立しているだけでなく、ガードbが現在の状態で真であるということも言えます。

このことは、cについての（Pがcの終了時にも成立することの）推論の際にいくらかの情報を与えてくれます。 結局、規則の最終バージョンはこうなります:
               {{P /\ b}} c {{P}}
        ---------------------------------- (hoare_while)
        {{P}} WHILE b DO c END {{P /\ ~ b}}

命題Pは不変条件(invariant)と呼ばれます。

One subtlety in the terminology is that calling some assertion P a "loop invariant" doesn't just mean that it is preserved by the body of the loop in question (i.e., {{P}} c {{P}}, where c is the loop body), but rather that P together with the fact that the loop's guard is true is a sufficient precondition for c to ensure P as a postcondition. This is a slightly (but importantly) weaker requirement. For example, if P is the assertion X = 0, then P is an invariant of the loop WHILE X = 2 DO X := 1 END although it is clearly not preserved by the body of the loop.

WHILE規則を使うと、次のホーアの三つ組も証明できます...

もちろん、この結果は驚くことではないのです。 ふり返ってhoare_tripleの定義を見てみると、コマンドが停止した場合「のみ」に意味がある表明をしているのです。 もしコマンドが終了しないなら、なんでも望むものが事後条件として示せます。

コマンドが停止したときに関してのみ（しかも停止することを示すことなく）何が起こるかを議論するホーア規則は、「部分」正当性("partial" correctness)を記述していると言われます。 「完全」正当性("total" correctness)についてのホーア規則を与えることも可能です。 それは、コマンドが停止するという事実を組み込んだものです。 ただし、このコースでは部分正当性についてのみ説明します。

練習問題: REPEAT

練習問題: ★★★★, advanced (hoare_repeat)

この練習問題では、言語に新たなコマンドを追加します。 REPEAT c UNTIL b ENDという形のコマンドです。 REPEATの評価規則を記述し、このコマンドを含むプログラムについての評価規則と新たなホーア論理の規則を追加しなさい。 （評価規則についてはAuto章でも例として使っていますが、それを見ないでやってみましょう。）

REPEATはWHILEと同じように振舞います。 ただし、ループのガードが本体の実行の「後で」評価され、それが「偽」である間はループがくりかえされるという点が違います。 このことにより、本体は常に少なくとも1回は実行されることになります。

以下のcevalにREPEATの新たな規則を追加しなさい。 WHILEの規則を参考にして構いません。 ただし、REPEATの本体は1度は実行されること、ループの終了はガードが真になったときであることを忘れないで下さい。

上記からいくつかの定義のコピーし、新しいcevalを使うようにしました。

To make sure you've got the evaluation rules for REPEAT right, prove that ex1_repeat evaluates correctly.

Now state and prove a theorem, hoare_repeat, that expresses an appropriate proof rule for repeat commands. Use hoare_while as a model, and try to make your rule as precise as possible.

For full credit, make sure (informally) that your rule can be used to prove the following valid Hoare triple: X > 0 REPEAT Y ::= X;; X ::= X - 1 UNTIL X = 0 END X = 0 /\ Y > 0

☐

Summary

So far, we've introduced Hoare Logic as a tool for reasoning about Imp programs. The rules of Hoare Logic are:

---

(hoare_asgn) Q [X |-> a] X::=a Q

---

(hoare_skip) P SKIP P P c1 Q Q c2 R

---

(hoare_seq) P c1;;c2 R P /\ b c1 Q P /\ ~ b c2 Q

---

(hoare_if) P TEST b THEN c1 ELSE c2 FI Q P /\ b c P

---

(hoare_while) P WHILE b DO c END P /\ ~ b P' c Q' P ->> P' Q' ->> Q

---

(hoare_consequence) P c Q In the next chapter, we'll see how these rules are used to prove that programs satisfy specifications of their behavior.

Additional Exercises

Exercise: 3 stars, standard (hoare_havoc)

In this exercise, we will derive proof rules for a HAVOC command, which is similar to the nondeterministic any expression from the the Imp chapter. First, we enclose this work in a separate module, and recall the syntax and big-step semantics of Himp commands.

The definition of Hoare triples is exactly as before.

Complete the Hoare rule for HAVOC commands below by defining havoc_pre and prove that the resulting rule is correct.

☐

Exercise: 4 stars, standard, optional (assert_vs_assume)

In this exercise, we will extend IMP with two commands, ASSERT and ASSUME. Both commands are ways to indicate that a certain statement should hold any time this part of the program is reached. However they differ as follows:

• If an ASSERT statement fails, it causes the program to go into an error state and exit.
• If an ASSUME statement fails, the program fails to evaluate at all. In other words, the program gets stuck and has no final state.

The new set of commands is:

To define the behavior of ASSERT and ASSUME, we need to add notation for an error, which indicates that an assertion has failed. We modify the ceval relation, therefore, so that it relates a start state to either an end state or to error. The result type indicates the end value of a program, either a state or an error:

Now we are ready to give you the ceval relation for the new language.

We redefine hoare triples: Now, {{P}} c {{Q}} means that, whenever c is started in a state satisfying P, and terminates with result r, then r is not an error and the state of r satisfies Q.