[Why3] How to Use Why3 (Theorem Prover Advent Calender)

この記事はTheorem Proving Advent Calendar 2011の16日目の記事です。（なお、Advent Calender の参加者も継続募集中です。）

前回はWhy3のインストールと動作確認を行いましたが、今回はWhy3 を使ったプログラミング検証について解説します。

素で Coq を使って手続き型的なコード(変数への破壊的代入を用いたコード)を証明する際には、Coq内DSLとして手続き的言語を実装して、Hoareトリプルを用いて言語の公理的意味論を実装して、参照や配列に関する公理ライブラリを準備して云々、という手間が必要になります。（PierceのSoftware FoundationsにImp:Simple Imperative Programsという章があります。あるいは当Advent Calenderのimunolionさんによる２日目の記事、Coqでセンター試験のBasicを解く、を参照下さい。）

Why3 を用いることで、上記の手間を省くことが出来ます。(そして運が良ければ自動証明で片が付きます。)
Why3 では、Why3ML というML系言語でプログラムを実装出来ます。その際に、コード中にアノテーションとしてHoareの事前事後条件、ループ不変条件などを記述します。Why3 は参照を用いた破壊的代入や for-loop などの手続き言語的な構文をサポートします。そして事前事後条件やループ不変条件から weakest precondition を計算してくれ、証明課題を生成します。

マニュアルのプログラム例は VSTTE 2010 の課題から取られているようで、その最初の問題を Why3 で解いてみます。 課題は

自然数 $N$ 個を格納した配列の要素の最大値 $\mathrm{max}$, 要素の和 $\mathrm{sum}$ について $\mathrm{sum} \le N \times \mathrm{max}$

が成り立つことを示せ、というものです。

■Why3ML でのプログラミング

上の問題を Why3ML 言語で実装したものです。まぁ大体読めますよね。
ref を使うことで参照を作れます。!でderefでき、:= で再代入です。refはWhy3のライブラリとして定義されているので、興味のある人は modules/ref.mlw を読むと良いでしょう。a[i] のように配列の値を参照出来ますが、array も同様に array.mlw で定義されています。
{...} は事前事後条件、invariant {...} はループ不変条件です。事後条件の部分に課題が書かれています。

% cat max_sum.mlw 
module MaxAndSum

  use import int.Int 
  use import module ref.Ref
  use import module array.Array

  let max_sum (a: array int) (n: int) =
    { 0 <= n = length a /\ forall i:int. 0 <= i < n -> a[i] >= 0 }
    let sum = ref 0 in
    let max = ref 0 in
    for i = 0 to n - 1 do
      invariant { !sum <= i * !max }
      if !max < a[i] then max := a[i];
      sum := !sum + a[i]
    done;
    (!sum, !max)
    { let (sum, max) = result in sum <= n * max }

end

ここではforループが使用されていますが、Why3MLではloop-end, while-do-done, do-done などループ構文が複数用意されています。例外処理の構文はraiseで例外を投げて、try-with-endで例外を発生する箇所をガードする形。アサーションはassert, assume, check と同じようなものが３つ。パターンマッチ構文match-with-endもあります。構文の詳細はマニュアルを参照して下さい。

■Alt-Ergoでの自動証明

これをAlt-Ergoで自動証明してみます。

% why3ml -P alt-ergo max_sum.mlw
max_sum.mlw WP MaxAndSum WP_parameter max_sum : Unknown: Unknown (0.05s)
%

が、Alt-Ergoは失敗しました。さすがに自動証明は通りませんでした。

■Coq用の証明課題生成

Coqの証明課題も生成してみます。

% mkdir max_sum
% why3ml -P coq -o max_sum max_sum.mlw
% ls max_sum
max_sum_MaxAndSum_WP_parameter_max_sum.v
% cat max_sum/max_sum_MaxAndSum_WP_parameter_max_sum.v 
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Require Import ZArith.
Require Import Rbase.
Definition unit  := unit.

Parameter qtmark : Type.

Parameter at1: forall (a:Type), a -> qtmark -> a.

Implicit Arguments at1.

Parameter old: forall (a:Type), a -> a.

Implicit Arguments old.

Inductive ref (a:Type) :=
  | mk_ref : a -> ref a.
Implicit Arguments mk_ref.

Definition contents (a:Type)(u:(ref a)): a :=
  match u with
  | (mk_ref contents1) => contents1
  end.
Implicit Arguments contents.

Parameter map : forall (a:Type) (b:Type), Type.

Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.

Implicit Arguments get.

Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).

Implicit Arguments set.

Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
  forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
  a2) = b1).

Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
  forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
  a2) = (get m a2)).

Parameter const: forall (b:Type) (a:Type), b -> (map a b).

Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.

Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
  b1):(map a b)) a1) = b1).

Inductive array (a:Type) :=
  | mk_array : Z -> (map Z a) -> array a.
Implicit Arguments mk_array.

Definition elts (a:Type)(u:(array a)): (map Z a) :=
  match u with
  | (mk_array _ elts1) => elts1
  end.
Implicit Arguments elts.

Definition length (a:Type)(u:(array a)): Z :=
  match u with
  | (mk_array length1 _) => length1
  end.
Implicit Arguments length.

Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
Implicit Arguments get1.

Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
  match a1 with
  | (mk_array xcl0 _) => (mk_array xcl0 (set (elts a1) i v))
  end.
Implicit Arguments set1.

(* YOU MAY EDIT THE CONTEXT BELOW *)

(* DO NOT EDIT BELOW *)

Theorem WP_parameter_max_sum : forall (a:Z), forall (n:Z), forall (a1:(map Z
  Z)), (((0%Z <= n)%Z /\ (n = a)) /\ forall (i:Z), ((0%Z <= i)%Z /\
  (i <  n)%Z) -> (0%Z <= (get a1 i))%Z) -> ((((n - 1%Z)%Z <  0%Z)%Z ->
  (0%Z <= (n * 0%Z)%Z)%Z) /\ ((0%Z <= (n - 1%Z)%Z)%Z ->
  ((0%Z <= (0%Z * 0%Z)%Z)%Z /\ forall (max:Z), forall (sum:Z), (forall (i:Z),
  ((0%Z <= i)%Z /\ (i <= (n - 1%Z)%Z)%Z) -> ((sum <= (i * max)%Z)%Z ->
  (((0%Z <= i)%Z /\ (i <  a)%Z) /\ (((max <  (get a1 i))%Z ->
  (((0%Z <= i)%Z /\ (i <  a)%Z) /\ forall (max1:Z), (max1 = (get a1 i)) ->
  (((0%Z <= i)%Z /\ (i <  a)%Z) /\ forall (sum1:Z), (sum1 = (sum + (get a1
  i))%Z) -> (sum1 <= ((i + 1%Z)%Z * max1)%Z)%Z))) /\ ((~ (max <  (get a1
  i))%Z) -> (((0%Z <= i)%Z /\ (i <  a)%Z) /\ forall (sum1:Z),
  (sum1 = (sum + (get a1 i))%Z) -> (sum1 <= ((i + 1%Z)%Z * max)%Z)%Z)))))) /\
  ((sum <= (((n - 1%Z)%Z + 1%Z)%Z * max)%Z)%Z -> (sum <= (n * max)%Z)%Z)))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.

Qed.
(* DO NOT EDIT BELOW *)

%

■生成された証明課題をCoqで証明する。

まぁこれを Coq で証明すれば OK なんですが...。
見た目、すごい定理の様になっていますが、intuition すると3つの証明課題に分離されます。それを ring, omega などを駆使して各個撃破すれば OK です。証明するとこんな感じ。

(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
Require Import Omega.
Require Import Ring.
      rewrite H8. rewrite H7.
      cut((sum <= (i*get a1 i)%Z)%Z). intro.
        replace ((i+1)%Z*get a1 i)%Z with ((i*get a1 i)%Z + get a1 i)%Z.
          omega.
        ring.
      cut(((i*max)%Z <= (i*get a1 i)%Z)%Z). intro.
        omega.
      destruct i; try omega.
        eapply Zmult_le_compat_l; try omega.
      elim H5. simpl. auto.
  rewrite H7.
    replace ((i+1)*max)%Z with (i*max + max)%Z.
      omega.
    ring.
  replace (n-1+1)%Z with n in H3. auto.
    auto.
  omega.
Qed.
(* DO NOT EDIT BELOW *)

■まとめ

Coq を使うことで課題を証明出来ました。 今回は事前条件やループ不変条件をマニュアル記載の所与のものとしましたが、実際には正しくかつ充分なそれらを書くのはそれなりに知識が必要です。
ですが、とりあえずWhy3を使用することで、最弱事前条件を自動生成してくれるので、ひたすら定理を証明すれば良く、かなり楽になります。

■その先の話

Why3の上に更にKrakatoaを使うことで、Javaプログラムの検証が出来る、という話をKrakatoa and Jessieを用いた、Javaプログラムの正当性＆安全性証明(アルゴリズムもあるよ！)という記事でqnighyさんがAdvent Calenderの記事に書いていますのでそちらもご覧下さい。Krakatoaを用いたJavaプログラムの検証の場合は、intがZ(Coqの任意桁整数)でなくJavaと同じ32bit整数で扱われるので、より実用的ですが証明が大変です。

■宣伝

毎月１回週末に、新宿にて形式手法勉強会の Formal Methods Forum を開催しています。内容は Coq を中心とした各種形式手法（定理証明系とモデル検査など）についての勉強会です。東京近隣の方はぜひご参加を。（あと来年の１、２月の平日夜にCoq講習会を計画してます。もうちょっとしたらFMFとかで告知します。）