ズッキーニのプログラミング実験場

プログラミング + アカデミック + 何か面白いこと。 記載されているものは基本的に私が所属する団体とは関係がありません。

   Mar 25

Coqによる 証明駆動開発 超入門

by zuqqhi2 at 2015年3月25日
Pocket

証明駆動開発 とは

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

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を利用する環境が構築出来た!
    Coqtop-vim

    Windows

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

    Coqの使い方

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

    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 

    coqtop-vim1

    命題定義を入力したらコマンドモードで「:CoqGoto」と入力する。
    すると、vimに入力した文がcoqtopに送られ、coqtopコマンドを利用したとときに表示された結果が右側に出力される。
    証明駆動開発

    あとは、coqtopコマンドを利用したときと同様に証明すればよい。
    個人的にこれを使用している。

    coqide – GUI

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

    後はcoqtopコマンドを利用した時と同様に証明していく。

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

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

    ここでは、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コードが生成出来ていることが確認できる。

    Related Posts

    Pocket

    You can follow any responses to this entry through the RSS 2.0 feed. Both comments and pings are currently closed.