[Misc] 2011 Summary

2011年を振り返ってですが、

• 今年もFormal Methods Forumが続けられた。@kencoba さん他皆様のお陰だと思います。来年も継続して行きたい。
• RegExpライブラリが書けたのは嬉しかった。2012年も上半期に何か纏まった成果を出したいなぁ。
• 数学関係の読書会に参加した。@bonotake さん、@cocoatomo さん、@erutuf13 さんのおかげです。ありがとうございます。学部時代は20年ぐらい前のはずだが、昔勉強した数学、案外忘れてないものだなー。2012年はとりあえず群環体の入門書を終わらせ、2013年以降に繋げたいな。
• ICFP 2011は、聞いた話の全部が理解出来た訳じゃないけど楽しかったー。年休とって参加した甲斐がありました。途中体調崩したのは残念というか、適宜中休み入れないと駄目か。今後も年休取れるなら学会聞きに行きたいな。
• 名古屋のProof Cafeの皆様のご協力を得て、Proof Summit 2011を開催出来ました。時間調整にかなり失敗して発表者の皆様にはかなり迷惑をおかけしましたが、結果としては充実したイベントになったかなー。
• TPP 2011を聞きに行きました。これも勉強になり楽しかったです。来年(千葉大で開催らしい)とか、何か発表出来るといいなぁ。

来年も宜しくお願いします＞皆様。

[Coq] Group defined by one operation

通常、群$G$を定義するときは、演算 $\cdot : (G \times G) \rightarrow G$, と単位元 $e:G$, 逆元 $(\cdot)^{-1}:G \rightarrow G$ から定義しますが、$x/y := xy^{-1}$ を基本的な定義として群を定義することも出来ます。（$H \subset G$ が部分群であることを示すには $\forall x,\; y \in H,\;\; x/y \in H$ を示せば良い、など計算の手間が減って都合が良い。）

演算 $x/y : (G \times G) \ni (x,y) \mapsto xy^{-1} \in G$ が下記の公理を満たすならば、

• $a/a = b/b$
• $a/(b/b) = a$
• $(a/a)/(b/c) = c/b$
• $(a/c)/(b/c) = a/b$

$G$ は群になります。というのを Coq で証明しました。コードは https://github.com/tmiya/coq/blob/master/group/group2.v にも置いてあります。
群の法則の中では、結合則を示すのに苦労しました。

(** Group defined by one operation *)
(* Operator 'x/y' means xy^{-1}.
  Probe that '/' and four axioms obout it defines a group. *)

Section Group2.
Parameter G:Set.
(* G is not an empty set. At least one element exists. *)
Parameter g0:G. 
Parameter op:G->G->G.
Notation "a / b" := (op a b).
(* Axioms for / *)
Parameter G1: forall a b, a/a = b/b.
Parameter G2: forall a b, a/(b/b) = a.
Parameter G3: forall a b c, (a/a)/(b/c) = c/b.
Parameter G4: forall a b c, (a/c)/(b/c) = a/b.

Definition e:G := g0/g0.
Notation "1" := e.
Definition mult(a b:G) := (a/(1/b)).
Notation "a * b" := (mult a b).

Lemma op_refl_1 : forall a, a/a = 1.
Proof.
intro a. unfold "1". eapply G1.
Qed.

Lemma op_1 : forall a, a/1 = a.
Proof.
intro. unfold "1". rewrite G2. auto.
Qed.

Theorem left_id : forall a, 1*a = a.
Proof.
intro. unfold "1". unfold "*".
erewrite G3. eapply op_1.
Qed.

Theorem right_id : forall a, a*1 = a.
Proof.
intro. unfold "*". erewrite op_1.
erewrite op_1. auto.
Qed.

Definition inv(a:G) := (1/a).
Notation "! a" := (inv a) (at level 91).

Theorem left_inv : forall a, (!a)*a=1.
Proof.
intros. unfold "!". unfold "*".
rewrite G4. erewrite op_1. auto.
Qed.

Lemma inv_inv : forall a, 1/(1/a) = a.
Proof.
intros.
replace (1/(1/a)) with (1/1/(1/a)).
 rewrite G3. eapply op_1.
erewrite op_1. auto.
Qed.

Theorem right_inv : forall a, a*(!a)=1.
Proof.
intros. unfold "!". unfold "*".
erewrite inv_inv. eapply op_refl_1.
Qed.

Lemma inv_op : forall a b, inv (a/b) = b/a.
Proof.
intros. unfold "!". unfold "1".
erewrite G3. auto.
Qed.

Lemma inv_idem : forall a, inv (inv a) = a.
Proof.
intros. unfold "!". eapply inv_inv.
Qed.

Lemma op_eq : forall a b c d,
 a/b = c/d -> b/a = d/c.
Proof.
intros.
replace (b/a) with (1/1/(a/b)).
 replace (d/c) with (1/1/(c/d)).
  rewrite H. auto.
 erewrite G3. auto.
erewrite G3. auto.
Qed.

Lemma op_mult : forall a b, (a/b)*b = a.
Proof.
intros. unfold "*". erewrite G4.
eapply op_1.
Qed.

Lemma rm_op_2 : forall a b c, a/c=b/c -> a=b.
Proof.
intros. assert(a/c*c = b/c*c).
 rewrite H. auto.
erewrite op_mult in H0.
erewrite op_mult in H0. auto.
Qed.

Lemma rm_op_1 : forall a b c, a/b=a/c -> b=c.
Proof.
intros. specialize(op_eq a b a c H). intro.
eapply (rm_op_2 b c a H0).
Qed.

Lemma mult_op : forall a b, (a*b)/b = a.
Proof.
intros. unfold "*".
replace (a/(1/b)/b) with (a/(1/b)/(1/(1/b))).
rewrite G4. rewrite op_1. auto.
replace (1/(1/b)) with b. auto.
erewrite inv_inv. auto.
Qed.

Lemma assoc_2 : forall a b c, a/(b/c) = a*c/b.
intros.
replace (a/(b/c)) with ((a*c)/c/(b/c)).
rewrite G4. auto.
rewrite mult_op. auto.
Qed.

Lemma assoc_3 : forall a b c, a*(c/b) = a*c/b.
intros. 
replace (a*(c/b)) with (a/(inv (c/b))).
unfold "!". replace (1/(c/b)) with (b/c).
rewrite assoc_2. auto.
replace (1/(c/b)) with (1/1/(c/b)).
rewrite G3. auto. rewrite op_1. auto.
unfold inv. unfold "*". auto.
Qed.

Lemma assoc_4 : forall a b c, a*(c*(inv b)) = a*c*(inv b).
intros. unfold inv.
replace (c*(1/b)) with (c/b).
replace (a*c*(1/b)) with (a*c/b).
eapply assoc_3.
unfold "*". rewrite inv_inv. auto.
unfold "*". rewrite inv_inv. auto.
Qed.

Theorem assoc : forall a b c, a*(b*c) = a*b*c.
intros.
replace c with (inv (inv c)).
eapply assoc_4.
eapply inv_idem.
Qed.
End Group2.

[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とかで告知します。）

[Blogger][LaTeX] Install MathJax

MathJax in Blogger (II) を参考にMathJaxを使える様にしてみた。

$$a^2+b^2=c^2$$

どうやら使えているみたい。

[Why3] Install of Why3 Tool (Theorem Prover Advent Calender)

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

Why3 をMacOS (Snow Leopard) に導入してみました。
Why3 は Why の後継で、Why というのはプログラム検証プラットホームです。Java や C のプログラムに注釈として事前事後条件などを書くと、why 言語という中間言語に一度処理され、Alt-Ergo などの自動証明器や Coq のような証明支援系に適した出力に変換してくれます。さらに上記を統合した GUI フロントエンドを提供します。その辺の話は昔作った発表資料(Slideshare)を参照して下さい。

■なぜ Why3 を学ぶのか
今年の11月に VSTTE 2012 Software Verification Competition という競技ソフトウェア検証イベントがありました。平日開催で忙しかったという理由もありますが、出された問題の多くが手続き型的コードの検証ということもあり、普通の Coq の証明の知識だけでは手が出ませんでした。そこで来年に活かそう、という理由で Why3 を学ぶことにしました。
実際問題として、手続き的に書かれたプログラムについて検証したいという需要は多いと思われます。（たとえ Coq などの定理証明系は純関数型的なコードと相性が良くても。）
Why3 と同様のツールに関しては CFML という OCaml コードの検証ツールについて @keigoi さんが記事をお書きになっていますので、そちらもご覧下さい --- というか CFML もいずれ動かしてみたいです。

■ Why3 導入
すでに Xcode, macports とか OCaml, Coq は導入済みと仮定します。
Why3 ダウンロードサイトよりversion 0.71のtarを入手し、適当なディレクトリで展開します。configure したら色々無いと判ったのでとりあえず導入。ocamlgraph は ports に無いので別途ここから入手。でも CoqIDE 動いてるのになんで lablgtk2 無いの？

% ./configure
略
% sudo port install lablgtk2% sudo port install caml-menhir
% sudo port install rubber
% sudo port install caml-sqlite3


ocamlgraph 導入
% cd ???/ocamlgraph-1.8.1
% ./configure
% make
% sudo make install
% sudo make install-findlib


why3 ディレクトリに戻る
% ./configure
                 Summary
-----------------------------------------
OCaml version           : 3.12.1
OCaml library path      : /opt/local/lib/ocaml
Verbose make            : no
Why IDE                 : yes
Why bench tool          : yes
Why documentation       : yes
Why plugins             : yes
Coq plugin support      : no  (not yet implemented)
TPTP parser             : yes
Menhir library          : no
hypothesis selection    : yes
profiling               : no
localdir                : no
% make


ここで why3-0.71/src/ide/gmain.ml の GSourceView2 を gSourceView2 に修正など苦労するが結局


File "gmain.ml", line 1180, characters 42-43:
Error: Syntax error: ')' expected
File "gmain.ml", line 1180, characters 25-26:
Error: This '(' might be unmatched


などのコンパイルエラーが消えず、GUIは諦めることにする。


% ./configure --disable-ide
% make clean; make
% sudo make install


各種ツールが /usr/local/bin/ に導入された。



■ 各種自動定理証明器の導入
基本的にどれかで証明出来れば良いと考えると、色々導入した方が有利なんですが、とりあえず Alt-Ergo だけ導入すれば雰囲気は味わえます。どれが一番強力な自動証明器かというのは良く解りません。

Alt-Ergo は Why3 のページから辿って、alt-ergo-0.93 の Mac 版をダウンロードするだけ (make 不要)。

CVC3 についても同様にして 64-bit Intel Mac OS X (Snow Leopard) dynamic library and executable cvc3 2.4.1 を導入。これは展開するだけ。

Yices も同様に Yices 1.0.31 をダウンロードして展開。

Gappa も同様に gappa 0.15.1 をダウンロード。INSTALL を読むと前提が GMP, MPFR, Boost なのでそれぞれダウンロードして導入。GMPは入手先サイトが無くなっていたので ports で代用し、 
% sudo port install gmp
% sudo port install mpfr
% sudo port install boost
% ./configure
GMPが見つからず失敗
% ./configure "CPPFLAGS=-I/opt/local/include" "LDFLAGS=-L/opt/local/lib"
成功
% make
% sudo make install
で代用。

■構成
インストールしたcvc3などにPATHを通して
% why3config --detect
します。なんかyicesが未サポートヴァージョン、cvc3が動かず、Alt-Ergo, Gappa, Coq だけという状況。一度構成したら
% why3 --list-provers
Known provers:
  alt-ergo (Alt-Ergo)
  coq (Coq)
  gappa (Gappa)
  yices (Yices)
と表示されます。証明器を追加したら再度同様に構成します。

■実行例
examples/に入っている

% cat hello_proof.why
theory HelloProof "My very first Why3 theory"

  goal G1 : true

  goal G2 : (true -> false) /\ (true \/ false)

  use import int.Int

  goal G3: forall x:int. x*x >= 0

end
%

を試してみましょう。ちなみにG2はそもそも間違っているので自動証明失敗して当然です。
Coq については出力先ディレクトリを予め作成しておいて、-o オプションで指定します。

% why3 -P alt-ergo hello_proof.why 
hello_proof.why HelloProof G1 : Valid (0.03s)
hello_proof.why HelloProof G2 : Unknown: Unknown (0.04s)
hello_proof.why HelloProof G3 : Valid (0.03s)
% why3 -P gappa hello_proof.why
hello_proof.why HelloProof G1 : Valid (0.00s)
hello_proof.why HelloProof G2 : Unknown: Unknown (0.00s)
hello_proof.why HelloProof G3 : Unknown: Unknown (0.00s)
% why3 -P yices hello_proof.why
hello_proof.why HelloProof G1 : Valid (0.00s)
hello_proof.why HelloProof G2 : Unknown: Unknown (0.00s)
hello_proof.why HelloProof G3 : Unknown: Unknown (0.00s) 

% mkdir hello

% why3 -P coq -o hello hello_proof.why
% ls hello
hello_proof_HelloProof_G1.v hello_proof_HelloProof_G3.v
hello_proof_HelloProof_G2.v 

% cat hello/hello_proof_HelloProof_G2.v 
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Require Import ZArith.
Require Import Rbase.
(* YOU MAY EDIT THE CONTEXT BELOW *)

(* DO NOT EDIT BELOW *)

Theorem G2 : False.
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.

Qed.
(* DO NOT EDIT BELOW *)

% 

G2を下記の様に正しく修正すると、


% grep G2 hello_proof.why
  goal G2 : (true -> false) \/ (true \/ false)
% why3 -P alt-ergo hello_proof.why
hello_proof.why HelloProof G1 : Valid (0.03s)
hello_proof.why HelloProof G2 : Valid (0.03s)
hello_proof.why HelloProof G3 : Valid (0.03s)
%

上記の様に自動証明に成功します。 ツールの導入が終わったので、次回は Why3 を用いたプログラム開発に付いて説明します。

■宣伝
毎月１回週末に、新宿にて形式手法勉強会の Formal Methods Forum を開催しています。内容は Coq を中心とした各種形式手法（定理証明系とモデル検査など）についての勉強会です。東京近隣の方はぜひご参加を。