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