■

変数 X がある数 x を持つ状態で fact_com を実行すると、 変数 Y が x の階乗の値を持つ状態で停止する、ということを示したくなります。

これを示すため、ループ不変式 (loop invariant) という重要な概念を使います。

Z := X;
Y := 1;
WHILE not (Z = 0) DO
  Y := Y * Z;
  Z := Z - 1
END

というプログラムにおいて

Fixpoint real_fact (n:nat) : nat :=
  match n with
  | O => 1
  | S n' => n * (real_fact n')
  end.

Definition fact_invariant (x:nat) (st:state) :=
  (st Y) * (real_fact (st Z)) = real_fact x.

Theorem fact_body_preserves_invariant: ∀ st st' x,
     fact_invariant x st →
     st Z <> 0 →
     fact_body / st &#8659; st' →
     fact_invariant x st'.

Theorem fact_loop_preserves_invariant : ∀ st st' x,
     fact_invariant x st →
     fact_loop / st &#8659; st' →
     fact_invariant x st'.

Theorem guard_false_after_loop: forall b c st st',
     (WHILE b DO c END) / st || st' ->
     beval st' b = false.
Proof.

• Loopの前に成り立つ。
• Loopの各ステップの前後で成り立つ。
• Loopの後にも成り立つ。

これがどのように重要な概念なのか、どう有用なのかよくわからん。