Home >

news ヘルプ

論文・著書情報


タイトル
和文:定理証明支援系Coqへの対話的修正機構の導入 
英文:Implementation of an Interactive Correction Mechanism for Coq 
著者
和文: 森口草介, 渡部卓雄.  
英文: Sosuke Moriguchi, Takuo Watanabe.  
言語 Japanese 
掲載誌/書名
和文:情報処理学会論文誌プログラミング（PRO） 
英文:IPSJ Transactions on Programming 
巻, 号, ページ Vol. 5    No. 4    pp. 27-38
出版年月 2012年9月4日 
出版者
和文:情報処理学会 
英文:Information Processing Society of Japan 
会議名称
和文: 
英文: 
開催地
和文: 
英文: 
公式リンク http://id.nii.ac.jp/1001/00083703/
 
アブストラクト 定理証明支援系Coqに対する，対話的にプログラムの変更・修正を行うための手法を提案し，その手法をCoqに組み込んだECoqを実装する．定理証明支援系によるプログラムの検証は，プログラムがある性質を満たすという証明により行われる．この証明はプログラムの構造や記述と非常に強く結び付いているため，プログラムを変更した場合，証明もまたその変更に依存した変更を行わなければならない．しかし，プログラムと証明の一貫性を保つために必要な変更箇所は，たとえばコンストラクタの追加という簡単な変更に限った場合であっても，既存の証明支援系では見つけにくい場合がある．このような問題に対処するため，我々はCoqで検証を行ったプログラムと証明に対して，その一貫性を保ちつつ変更するための手法を提案する．本論文で提案する手法では，コンストラクタの追加を行い，変更が必要な箇所を利用者に提示する．このとき，コンストラクタを追加する型だけではなく，宣言時の状態やその型を利用する他の型などの情報を用いるため，本手法はCoqの内部に組み込むことを前提としている．この機能は，変更が必要な箇所を対話的に修正するものであるため，我々はこれを対話的修正機構と呼ぶ．本論文で紹介するECoqは，コンストラクタの追加を行うコマンドをCoqに追加したものである．ECoqを用いることで，利用者はソースコードに直接コンストラクタを追加して得られるエラーメッセージより細かい粒度での情報が得られる．特にECoqは，通常決してエラーが起こらないが，修正する可能性のある箇所を指摘することで，利用者が修正箇所を見つける補助を行う．本論文では，例題を通じてエラーメッセージが出ない箇所をECoqが提示できることを確認する．

©2007 Institute of Science Tokyo All rights reserved.