証明支援系Coqのプログラムに対する対話的修正機構の提案

概要

論文の詳細を見る
証明支援系 Coq のプログラムに対する対話的修正機構を提案する.証明支援系はプログラムなどの正しさを証明するために利用されている.しかし,Coq による証明は対象となる体系の定義に密接に関連しているため,定義のわずかな修正に対して多くの不整合が発生する.このような不整合に対し,場所の確認を Coq からのエラーによって発見するという,退屈で,かつ誤りを組み込みやすい作業で行うことが一般的になっている.提案する機構を組み込んだ証明支援系を用いることにより,この作業を簡易化することができる.対話的修正機構は修正箇所の記述を受け取ることで,その修正によって不整合が生じた箇所を提示することができる.また,この提示された箇所をもとに修正を対話的に行うことを可能にしている.本発表で提案している Coq における対話的修正機構では,帰納型に新たなコンストラクタを追加することと,そのコンストラクタに対応するデストラクタの拡張を行う機能を持っている.このように機能としては非常に制限されているが,それにより非常に高い再利用性を得ることができる.本発表では,不整合のある箇所の検出方法と,制限の詳細について述べる.
2011-09-22