| 研究課題/領域番号 |
15K12007
|
|---|
| 研究機関 | 筑波大学 |
|---|
研究代表者 |
亀山 幸義 筑波大学, システム情報系, 教授 (10195000)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| キーワード | 定理証明系 / 形式検証 / 証明の自動化 / プログラム抽出 / 証明探索 / 副作用 / 証明の生成 |
|---|
| 研究実績の概要 |
研究初年度にあたり、証明支援系Coq およびその上のライブラリであるSSReflectについて調査検討を行った。特に、コントロールオペレータに関する研究を題材として、証明支援系を用いて形式検証する課題に取り組み、証明のリファインメンと、証明項目の抽出、抽出コードの改善手法などの成果を得た。
（１）コントロールオペレータについての研究を行い、これらの検証について検討した。特に、前年度得られた結果型変更の機能を、その機能がないプログラム言語で実現するためのプログラム変換の定式化を行った。この成果は Workshop on Continuationのpost-proceedingsに採択された。
（２）コントロールオペレータcall/ccとshift/resetおよびそれに対するCPS変換をCoqで形式化し、call/ccをshift/resetでマクロ表現する方式の正当性を形式検証した。このためには模倣関係を形式化する必要があるが、精度の粗い関係からはじめてCoqでの検証失敗例から学んで、徐々に改善することにより、正しい模倣関係を得るための手法について検討した。この成果は国内の定理証明系ミーティングであるTPPで発表した。
（３）SSReflectは、Coqにおける有限的対象に関する証明を（半）自動化するための強力な道具であるが、証明の人手を減らすことに主眼があるため、SSReflectを使って作成した証明から抽出したプログラムは、効率が非常に悪くなることが多い。これを改善するため「有限集合」をあらわす型の定義を改善し、証明にかかる手間をほとんど変更せずに、抽出コードの実行効率をあげる手法を提案した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
研究計画は非常に野心的であったが、3年計画の初年度に、研究発表できる成果（異なる発想にもとづく研究の端緒）が4件でてきている。ただし、これらの成果は1件を除いては萌芽的なものであり、今後完成度をあげる必要がある。
|
| 今後の研究の推進方策 |
初年度に得た萌芽的なアイディアをもとに、研究の完成度を上げ、査読付き国際会議での採択を目指す。とくに注力するのは、（1）マルチステージ証明記述言語として、コントロールオペレータなどの副作用を持ち、表現力が高い言語を設計して安全性を定式化および保証すること、（2）この言語と既存の Ltac, Mtacなどの証明記述言語との比較検討をすることの2点である。
|
| 次年度使用額が生じた理由 |
本年度は研究の端緒をつかむためCoqとSSReflectを用いた、形式検証の実例構築に大部分の時間を費やした。現段階では、巨大なメモリを要する証明探索はしていないので、このためのハードウェアは、既存のノートPCで済ませることができた。かかった経費は、マルチステージプログラミングおよび定理証明系Mizarの専門家を招聘する旅費のみであったため、未使用額が生じた。
|
| 次年度使用額の使用計画 |
上記で端緒をつかんだ4つの研究を発展させるため、平成28年度は学生に対する謝金を支出してシステムを構築するとともに、よりメモリの多いPC購入などに未使用額を使う。また、成果を積極的に国際会議等で発表するための費用として使用することを計画している。
|
