証明駆動開発 とは

証明駆動開発 とは証明によってプログラムが期待通りの性質を有しているかを確かめながら開発する手法のこと。
ユニットテストの一部で使用可能な方法。
証明駆動開発 での流れは参考サイトに記載されているように以下の流れで行う。

1.対象プログラムが持つべき性質を洗い出す
2.Coqでプログラムを書く
3.書いたプログラムの性質を証明する
4.他の言語のコードに出力する

参考サイトに証明の仕方については記述されているため、このページでは 証明駆動開発 にのみ焦点を当てる。

参考になるサイト

• coqによる 証明駆動開発 とcoqideの使い方：
  http://d.hatena.ne.jp/zyxwv/20090922/1253643926
• coqtopの使い方：
  http://www.iij-ii.co.jp/lab/techdoc/coqt/
• coqtop-vimの使い方：
  http://d.hatena.ne.jp/eagletmt/20110515/1305479711
• Coqでの証明方法：
  http://www.slideshare.net/tmiya/coq-tutorial

Coqのインストールと開発環境構築

開発環境構築

Linux

単純にapt-getでcoqをインストールすれば使用可能になる。

$ sudo apt-get install coq

vimでシェルを見ながら作業出来るようにするためにvimprocを導入する。

$ mkdir ~/tmp
$ cd ~/tmp
$ git clone https://github.com/Shougo/vimproc.git
$ cd vimproc
$ make -f make_unix.mak
$ cp -r autoload/* ~/.vim/autoload/
$ cp -r plugin/* ~/.vim/plugin

次にcoqtop-vimをインストールする。

$ git clone https://github.com/eagletmt/coqtop-vim
$ cd coqtop-vim
$ cp autoload/coqtop.vim ~/.vim/autoload/
$ cp plugin/coqtop.vim ~/.vim/plugin

これでvimでcoqを利用する環境が構築出来た！

Windows

http://coq.inria.fr/downloadこのサイトからCoqIdeをダウンロードしてインストールする。

Coqの使い方

ここでは参考サイトでも紹介されている以下の命題の証明を通して各ツールの使用方法について紹介する。
なお、ここではProof-editing modeを使用して証明する。

coqtop – インタプリタ

インタプリタを起動するにはcoqtopコマンドを使用する。

$ coqtop
Welcome to Coq 8.3pl4 (April 2012)

Coq <

このcoqtopを使用して実際に証明を行ってみる。
まずは、命題の定義を行う。「すべての」はforallで「命題A」はA : Propで
「AならばA」はA->Aとすればいい。

Coq < Goal forall (A : Prop), A -> A.
1 subgoal

  ============================
    forall A : Prop, A -> A

Unnamed_thm <

次に前提を全部出す。これにはintrosタクティクを使用する。

Unnamed_thm < intros.
1 subgoal

  A : Prop
  H : A
  ============================
    A

Aの型Prop、Aが真だという仮定Hが取りだされた。
あとは、Aが真だということを証明すればいい。
これは仮定Hにあるから、これをapplyタクティクを使って適用すれば証明が終了する。

Unnamed_thm < apply H.
Proof completed.

Unnamed_thm < Qed.
intros.
apply H.

Unnamed_thm is defined

Coq < Ctrl+D

$

終わる時は最後にCtrl+Dを入力すればいい。

coqtop-vim – vimプラグイン

ここではvimを使用して証明をする。
vimを起動して、vimのコマンドモードで「:CoqStart」と入力するとプログラミング用とは別のCoq用のウィンドウができる。

$ vim reflect.v 

命題定義を入力したらコマンドモードで「:CoqGoto」と入力する。
すると、vimに入力した文がcoqtopに送られ、coqtopコマンドを利用したとときに表示された結果が右側に出力される。
あとは、coqtopコマンドを利用したときと同様に証明すればよい。
個人的にこれを使用している。

coqide – GUI

インストールしたCoqIdeを起動する。
左側のウィンドウに証明を記入していく。
CoqIdeでは下向き矢印をクリックすることで証明を進められる。
後はcoqtopコマンドを利用した時と同様に証明していく。

CoqIdeでは便利なウィンドウがある。このウィンドウでは、定義したプログラムを実行したり、様々な情報を見ることが出来たりする。
画像の赤い枠で囲まれた部分をクリックすることでそのウィンドウを出すことができる。

証明駆動開発チュートリアル

ここでは、coqtop-vimを使用してリストの結合プログラムを証明駆動開発を開発してみる。

1.対象プログラムが持つべき性質を洗い出す

一般的なリストについて考えている場合、
少なくとも以下の2つの性質はリストの結合プログラムは持たなければならない。

a. リストAに空のリストBを結合させた結果はリストAに等しい。
b. リストA,B,CについてA::B::Cというように三つのリストを結合する場合、
リストAとBを結合させてからリストCを結合させた場合((A::B)::C)と、
リストBとCを結合させてからリストAを結合させた場合(A::(B::C))は等しい。

2.Coqでプログラムを書く

リストの結合をするプログラムをCoqで書いてみる。

Require Import List.
Fixpoint myapp (A : Type)(l l' : list A) : list A :=
  match l with
  | nil => l'
  | x::xs => x :: (myapp A xs l')
  end.

リストを使用するときはRequire Import Listでインポートする。

3.書いたプログラムの性質を証明する

a.空リストを結合しても変わらない

Theorem app_nil_r : forall (A : Type)(l : list A), myapp A l nil = l.
intros.
induction l.
reflexivity.
simpl.
apply (f_equal (cons a)).
apply IHl.
Qed.

b.結合結果はリストの結合順番に依存しない

Theorem app_assoc : forall (A : Type)(l1 l2 l3 : list A), myapp A l1 (myapp A l2 l3) = my
app A (myapp A l1 l2) l3.
intros.
induction l1.
reflexivity.
simpl.
f_equal.
apply IHl1.
Qed.

これで、定義したmyapp関数が持つべき性質を持っていることが証明された。

4.他の言語のコードに出力する

最後に、作成したmyapp関数をHaskellのコードに出力してみる。
現在のcoqで標準でサポートしているのはOcaml、Haskell、Schemeの3言語のみである。
末尾に以下の3行を追加する。

Extraction Language Haskell.
Extract Inductive list => "([])" ["[]" "(:)"].
Extraction "myapp" myapp.

作成したコードを保存して終了し、coqcコマンドでHaskellコードを生成する。

$ coqc myapp.v

作成したコードmyapp.hsを開いてみると、

module Myapp where

import qualified Prelude

myapp :: (([]) a1) -> (([]) a1) -> ([]) a1
myapp l l' =
  case l of {
   [] -> l';
   (:) x xs -> (:) x (myapp xs l')}

というようにHaskellコードが生成出来ていることが確認できる。