2014 Fiscal Year Research-status Report
ゲーム意味論に基づくリファインメント型の拡張とその応用
| Project/Area Number |
25730035
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
海野 広志 筑波大学, システム情報系, 助教 (80569575)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | リファインメント型 / 依存型 / 関係的仕様 / ホーン節制約解消 / 帰納的定理証明 / ゲーム意味論 / トレース意味論 / 抽象解釈 |
|---|
| Outline of Annual Research Achievements |
本研究では、リファインメント型システムをゲーム意味論に基づいて拡張することによって、既存手法よりも広いクラスのプログラムと仕様の自動検証を可能とすることを目指している。本年度は以下の成果が得られた。
1. リファインメント型の意味論の拡張：前年度に定式化した、値呼び関数型プログラム言語の操作的意味論の一種であるトレース意味論と、表示的意味論の一種であるゲーム意味論 [Honda and Yoshida 1997] との対応を与えた。さらに、リファインメント型システムがそれらの意味論の抽象解釈として定式化できることを示した。これらの成果によって、従来、操作的意味論・表示的意味論・抽象解釈それぞれの文脈で別々に研究されてきた技術を、リファインメント型システムを拡張するための基盤技術として一緒に用いることが可能になった。
2. リファインメント型システムの拡張：プログラムの完全正当性の検証を可能とするための拡張およびプログラムの（angelic/demonic）非決定的について柔軟に推論できるようにするための拡張を行った。
3. リファインメント型推論法の拡張：単調性・可換性・結合性といった関係的仕様を自動的に検証するためのリファインメント型推論法の設計・実装を行った。本手法では、帰納的定理証明とホーン節制約解消という従来別々に研究されてきた技術を相補的に組み合わせることによって、従来手法では困難であった関係的仕様の検証を可能とした。そして、リファインメント型推論の核となるホーン節制約解消のために、既存アルゴリズムでは解けない多くの問題を解くことが可能な新しいアルゴリズムの設計・実装を行った。さらに、ある1階の理論で表現可能な解が存在する場合は、必ず有限時間内に解を求めることができるという望ましい性質を持ったアルゴリズムの設計・実装も行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
研究実績の概要で述べたとおり、リファインメント型の意味論に関して当初の計画通りの理論的成果が得られている。関係的仕様検証のためのリファインメント型拡張に関しては、当初の予定とは（型システム・型判定法の拡張は最小限にとどめ、型推論法の拡張によって関係的仕様検証を可能にしたという点で）若干異なるアプローチをとってはいるが、当初27年度に行う予定であった型推論法の実装・評価が26年度中に概ね完了したという点で当初の計画以上の進展が得られている。さらに、リファインメント型システムおよび型推論法の拡張に関して当初予定していなかった様々な成果が得られている。特に、プログラムの非決定的の柔軟な推論に関する成果をまとめた論文が、システム検証に関するトップカンファレンスであるCAV2015に採録されたり、ホーン節制約解消アルゴリズムに関する成果をまとめた2つの論文が採択率25%前後の難関国際会議であるTACAS2015とESOP2015に採録されたりしている。
|
| Strategy for Future Research Activity |
今後も計画通りに研究を進める。26年度中に得られたリファインメント型の意味論および型システム・型推論法の拡張に関する成果は順次論文にまとめてトップカンファレンスに投稿する。
|
| Causes of Carryover |
次年度使用額が生じた主な理由は26年度中にあげた複数の研究成果の外部発表が27年度中に行われることになったためであり、26年度に予定していた旅費と学会参加費について、未使用額が生じた。
|
| Expenditure Plan for Carryover Budget |
次年度使用額は26年度にあげた研究成果の外部発表のための旅費・学会参加費として使用する。
|
