Isabelleによるプログラム検証の例

4 min read読了の目安(約3700字

はじめに

定理証明系 Isabelle を使ってプログラムの検証を行う例を紹介します.プログラム導出のヒューリスティクスも2つ紹介します.

定理証明系 Isabelle について

問題:自然数の平方根の近似値

与えられた自然数 n に対して,平方根の近似値を自然数の範囲で求める問題を考えます.

x=\lfloor\sqrt{n}\rfloor

ここで \lfloor a \rfloor は実数 a 以下の最大の整数です.floor 関数といいます.

問題を分析する

floor 関数の性質から

x \le \sqrt{n} < x + 1

両辺を2乗して

x * x \le n < (x + 1) * (x + 1)

これならば加算,乗算と比較だけで構成されているので扱いやすくなりました.

Isabelle の証明スクリプトと Hoare 論理ライブラリ

Isabelle には命令型プログラムの検証を行うための Hoare 論理のライブラリが用意されています.

命令は4つあります:

  • 空文 SKIP
  • 代入文 変数 :=
  • 条件文 IFTHENELSEFI
  • ループ WHILEINV {ループ不変条件式} DOOD

文の連接はセミコロンで表します.

証明スクリプト全体の構造は以下のようになります.

theory NatSqrt imports "~~/src/HOL/Hoare/Hoare_Logic" begin

theorem
 "VARS (x::nat)
  {True}
   ?
  {x * x ≤ n ∧ n < (x + 1) * (x + 1)}"
apply(vcg)
apply(auto)
...

証明したいプログラムの構造は

VARS 変数並び {事前条件} プログラム {事後条件}

となっています.

メソッド vcg を使うと,このプログラムを論理式に変換してくれます.

プログラム導出のヒューリスティクス 1

x をなんらかの値で初期化し,ループで目的の値を求めるという戦略をとることを決めたとしましょう.

ゴールである事後条件は2つの式 x * x ≤ nn < (x + 1)*(x + 1) の論理積になっています.
このようなときに使えるヒューリスティクスは,一部の項をループ不変条件にして,残りの否定をループの終了条件にすることです.そうすればループ終了後には自動的に事後条件が成り立つからです.

いまの場合,積項は2つしかありませんから,どちらかをループ不変条件にします.ループ不変条件はループに入る直前で成り立っていなければいけませんから,かんたんに成り立たせることのできる方を選びましょう.

x = 0 とすれば x * x ≤ n が成り立ちますから,こちらをループ不変条件にします.するとプログラムは次のようになります:

theorem
 "VARS (x::nat)
  {True}
  x := 0;
  WHILE n ≥ (x + 1) * (x + 1)
  INV {x * x ≤ n}
  DO
    x := x + 1
  OD
  {x * x ≤ n ∧ n < (x + 1) * (x + 1)}"
apply(vcg)

vcg メソッドを適用すると,次のように3つの式に変換されます:

proof (prove)
goal (3 subgoals):
 1. ⋀x. True ⟹ 0 * 0 ≤ n
 2. ⋀x. x * x ≤ n ∧ (x + 1) * (x + 1) ≤ n
    ⟹ (x + 1) * (x + 1) ≤ n
 3. ⋀x. x * x ≤ n ∧ ¬ (x + 1) * (x + 1) ≤ n
    ⟹ x * x ≤ n ∧ n < (x + 1) * (x + 1)

上から順に,ループ入口でのループ不変条件成立,ループ本体でのループ不変条件成立,ループ脱出後の事後条件成立を表します.

3つとも auto メソッドで自動的に証明できます.

選ぶ積項を入れ替える

n < (x + 1) * (x + 1) の方をループ不変条件にした場合はどうでしょうか.これを成立させるかんたんな x の初期値としては n を選べばいいでしょう.そうすると今度は x を減少させていくことになります.

theorem
 "VARS (x::nat)
  {True}
  x := n;
  WHILE x * x > n
  INV {n < (x + 1) * (x + 1)}
  DO
    x := x - 1
  OD
  {x * x ≤ n ∧ n < (x + 1) * (x + 1)}"

こちらは auto だけでは証明できませんでしたが,sledgehammer を呼び出したら証明できました.

プログラム導出のヒューリスティクス 2

\lfloor\sqrt{n}\rfloor は非減少なので2分探索が使えます.実際,事後条件は値をはさみうちにする形になっています.

x * x \le n < (x + 1) * (x + 1)

このようなときは変数を導入して一方の条件を置き換えます.
新しい変数 y を導入し,事後条件にある x + 1 を y に置き換えた式をループ不変条件にします.

x * x \le n < y * y

この y が x + 1 に等しくなったら事後条件と一致するわけですから,その否定をループ脱出条件にします.

theorem
 "VARS (x::nat) y
  {True}
  x := ?
  y := ?
  WHILE y ≠ x + 1                (* B *)
  INV {x * x ≤ n ∧ n < y * y}    (* A *)
  DO
     ?
  OD
  {x * x ≤ n ∧ n < (x + 1) * (x + 1)}"

初期値はどうでしょうか.x は 0 でよいでしょう.y は n にすると n = 0 のときに n < y * y が成り立たないので n + 1 とします:

theorem
 "VARS (x::nat) y
  {True}
  x := 0;                (* C *)
  y := n + 1;            (* D *)
  WHILE y ≠ x + 1
  INV {x * x ≤ n ∧ n < y * y}
  DO
     ?
  OD
  {x * x ≤ n ∧ n < (x + 1) * (x + 1)}"

ループ本体は2分探索です.変数 z を導入して x と y の中央値を計算します.

theorem
 "VARS (x::nat) y z
  {True}
  x := 0;
  y := n + 1;
  WHILE y ≠ x + 1
  INV {x * x ≤ n ∧ n < y * y}
  DO
    z := (x + y) div 2;
    IF z * z ≤ n THEN
      x := z
    ELSE
      y := z
    FI
  OD
  {x * x ≤ n ∧ n < (x + 1) * (x + 1)}"

z * z ≤ n ならば x の条件と同じ,逆ならば y の条件と同じですから,それぞれ x, y にそのまま z を代入すれば済みます.

証明は auto だけで自動的にできました.

おわりに

Isabelle の Hoare 論理ライブラリについて紹介しました.プログラム導出のヒューリスティクスを2つ紹介しました.

参考文献