CFML

以前に、CFMLというものがあるというのを教えてもらった(のは一ヶ月半前)ので、触ってみた。Characteristic Formula generator for MLの略らしい。サイトの下の方に論文リストもあるし、色々なアルゴリズムを証明した例もある
http://www.chargueraud.org/softs/cfml/

Coqのようなproof assistantにしろ、Alloyのようなモデル検査器にしろ、人間の考えの正当性を確認するには使えても、実際のコードの正当性の確認とは乖離がある。CoqのExtractというのはあるけど、限りなくバグが少ないとしても遅いコードとかには価値がないケースは多いし、そもそも、どっかの誰かが書いたコードが既にあった時、どうすんのかみたいな話もあるので、色々困る。というわけで、直接コードの検証をしましょうというのが趣旨だと思う

なんかCoq-8.4じゃないと動かないらしいので、漸くインストール

#-- install coq-8.4pl1
#sudo apt-get install ocaml camlp5
wget http://coq.inria.fr/distrib/V8.4pl1/files/coq-8.4pl1.tar.gz
tar xzvf coq-8.4pl1.tar.gz
cd  coq-8.4pl1/
./configure -local
make
cd ..
export PATH=`pwd`/coq-8.4pl1/bin:$PATH

#-- install CFML
svn checkout svn://scm.gforge.inria.fr/svn/cfml/branches/v1 cfml
make init
make depend
make
export CFML=`pwd`
export PATH=$CFML:$PATH

で、使い方
(1)Ocamlコード(例えばHalf.mlとする)を書いて
main.byte -rectypes -I $CFML -I $CFML/camllib -I $CFML/imper -I $CFML/user -I $CFML/okasaki -I $CFML/tlc Half.ml

(2)すると、Half_ml.vとかが生成される(このファイルに書いてあるのが、characteristic formulaというものらしい)のでCoqを起動
coqtop -I $CFML -I $CFML/camllib -I $CFML/imper -I $CFML/user -I $CFML/okasaki -I $CFML/tlc -l Half_ml.v

(3)後は普通にCoqで、Ocamlで書いた関数の示したい性質を書いて証明する

とりあえず、user/Demo.mlにある例として、

let rec half x =
  if x = 0 then 0
  else if x = 1 then assert false
  else 1 + half(x-2)

みたいのを考えて、"x=n+n->half x=n"という性質を証明することを考える。

Characteristic Formulaは生成されたファイルを読むと、よく分からんことになってるけども、Coqで"Print half_cf."とか打つと

half_cf :
forall K : int -> (hprop -> (int -> hprop) -> Prop) -> Prop,
is_spec_1 K ->
(forall x : int,
 K x
   (_If ((fun _y _z : int => _y '= _z) x 0) Then Ret 0
    Else (_If ((fun _y _z : int => _y '= _z) x 1) Then
          Fail Else (Let _x10 := App half ((x - 2)%I) ; in
                      Ret (1 + _x10)%I)))) ->
is_spec_1 K /\ (forall x1 : int, K x1 (AppReturns half x1))

とか返ってくる。よく分からんけど、雰囲気は分かる。half関数そのものは、Parameterとして定義されていて

Hint Extern
1 (RegisterCf half) => Provide half_cf.

とか書いてある。まぁ、このへんよく分かってなくても証明できるっぽい

で、証明する命題は、以下のような感じで書ける

Lemma half_spec :
  forall x n, n >= 0 -> x = n+n -> App half x; [] \[=n].

App half x;の後ろにある最初の[]には事前条件を書くらしい。今は何もない。2つ目の\[=n]は事後条件で、返り値がnに等しいという意味。論文にはAppの型はfoall A B,Func -> A -> hprop -> (B->hprop) -> Propだと書いてある(二変数以上の場合も使えるようになっているので、CoqでPrint Appしてもエラーだけど)。Ocamlの型からCoqの型への変換は結構アバウトで、関数は全部Func型になるらしい。で、一個目のhpropが事前条件、2個目の(B->hprop)が事後条件

これを

Lemma half_spec :
  Spec half (x:int) |R>>
    forall n, n >= 0 -> x = n+n -> R [] (\= n).

という風にも書ける模様。分かりやすいかどうかは微妙と思うけど

証明は、色々新しいtacticがあって、また覚えるのかよ！って感じ。Ocamlの方も覚束ないので二倍辛い

Set Implicit Arguments.
Require Import CFLib LibInt LibWf.

Lemma half_spec :
  forall x n, n >= 0 -> x = n+n -> App half x; [] \[=n].
Proof.
  intros x. 
  induction_wf IH: (int_downto_wf 0) x.
  intros n P D. 
  (* halfのcharacteristic formulaを展開する感じ? *)
  xcf_app.
  (* halfのif文を場合分け *)
  xif.
    (* n+n=0 -> (Ret 0) [] (\= n)を示す(return 0した結果がn) *)
    xret. 
    hsimpl. 
    auto with maths.
    (* 更にif文の場合分け *)
    xif.
      (* n+n=1 -> Fail [] (\= n)を示す *)
      xfail. auto with maths.
      (* x=n+n -> y=half (x-2) -> y+1=nに相当 *) 
      xlet.
        xapply (>> IH (x-2) (n-1)).
          auto with maths.
          auto with maths.
          auto with maths.
          hsimpl.
          auto.
        xret. hsimpl. rewrite H0. omega.
Qed.

一応、二変数の例(これも、user/Demo.vにある)

Require Import CFLib.
(* let add x y = x + y *)
Lemma add_spec : forall x y,App add x y; [] \[=x+y].
Proof.
  intros x y.
  xcf_app. xret. hsimpl.
  auto.
Qed.

まぁ、Coqで書けるプログラムは何とかなりそうな気もするけど、CFMLの面白いところは、代入とかを含む手続き的なプログラムの検証もできるところだと思う。例は、CFMLのimperディレクトリに沢山ある。例えば、imper/Loops.mlには

let incr_for k r = (for i=1 to k do (incr r) done)

とかある

imper/Loops.mlでは、k>=0に対して、incr_for k rによって、rの値がk増えるという命題を書いているけど、証明はskipでとばしている。特殊な場合として、incr_for 0 rすると、rの値が変わらないことを証明して見る(帰納法の最初のステップだけやったともいう)。今度は、ちゃんと事前条件が出てくる

Require Import CFLib.

(* let incr_for k r = (for i=1 to k do (incr r) done) *)
Lemma incr0_spec : 
  forall (r:loc) (n:int), App incr_for 0 r; (r ~~> n) (# r ~~> n).
Proof.
  intros r n.
  xcf_app.
  xfor.
  apply HS.
  split.
    math.
    intros;xret;hsimpl.
Qed.

まぁ、やっぱCoqで証明書くのは、めんどいなっていう。コード書くよりも証明書く手間が多いだろうなと思うと、そこがネックな気もするけど、実際の現場で書かれてるプログラムの99%は割と単純な処理な気もしなくもないので、工夫次第では意外と使えるのかもしれない。あと別に関数型何とかが殊更に好きでもないわたしにとっては、CやPythonでも使えそうな技なのが、面白いかなぁと思う。しかし、あんまり積極的に証明したいものも思いつかないので、続きは、いずれ気が向いた時にでも