| 研究課題/領域番号 |
25730035
|
|---|
| 研究種目 |
若手研究(B)
|
| 研究機関 | 筑波大学 |
|---|
研究代表者 |
海野 広志 筑波大学, システム情報系, 助教 (80569575)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| キーワード | リファインメント型 / ゲーム意味論 / トレース意味論 / 関係的仕様検証 / 停止性検証 |
|---|
| 研究概要 |
本研究では、リファインメント型システムをゲーム意味論に基づいて拡張することによって、既存手法よりも広いクラスのプログラムと仕様の自動検証を可能とすることを目指している。特に、関数型プログラムの「複数の関数呼び出しが関係した仕様」を扱うことのできる自動検証法の確立が、本研究の主目標である。25年度の主な成果は以下の3つである。
(1)主目標の達成度をはかるためのベンチマークとして、既存手法では自動検証に失敗していた様々なプログラムとその仕様を収集した。
(2)既存のリファインメント型システムのゲーム意味論的な解釈を与えることによって、拡張を行うために必要な数学的準備を行った。具体的には、まず、既存のリファインメント型システムの対象言語である、値呼び関数型プログラム言語のトレース意味論の定式化を行った。トレース意味論とは、プログラムの意味として、そのプログラムを実行した際に起こるイベント列の集合を割り当てるものであり、ゲーム意味論より素朴だが直観的で扱いやすいため、ゲーム意味論に本格的に取り組む前の練習台のつもりで研究を行った。その結果、研究計画段階ではゲーム意味論でなければ扱うのが難しいと予想していたイベント間の依存関係が、トレース意味論でも十分扱えることが分かった。また、ゲーム意味論とそのトレース意味論のインフォーマルな対応も明らかになったので、ゲーム意味論の代わりにトレース意味論を用いて、リファインメント型および型推論規則の解釈を与えた。
(3)既存のリファインメント型システムに対して2つの拡張を行った。1つ目の拡張によって、関数型プログラムの停止性の自動検証が可能となった。また、2つ目の拡張によって、木構造データを扱う関数型プログラムの検証精度が向上した。さらに、これら2つの拡張が、上述のトレース意味論ではどのように解釈されるのかを考察した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
研究実績の概要で述べたとおり、リファインメント型システムのゲーム意味論に基づく拡張を行うのに必要な基礎理論の構築と、研究目標の達成度をはかるためのベンチマークの作成に関して順調に成果が出ている。交付申請書に記載した研究計画では、25年度に拡張リファインメント型システムの設計・実装も行うことになっており、その点に関してはやや遅れているが、その分、26年度以降に行う予定であったリファインメント型システムの新しい応用に関する研究で著しい成果をあげることができた。特に、リファインメント型システムの停止性検証への応用を行った論文は、プログラミング言語分野において、欧州最高峰の国際会議ESOPに採択されている。また、木構造データを扱う関数型プログラムの自動検証への応用を行った論文は、国内会議PPLにおいて29報の論文の中から最優秀論文に選出されている。
|
| 今後の研究の推進方策 |
今後も計画通りに研究をすすめる。リファインメント型システムの新しい応用に関する研究は進んでいるが、ゲーム意味論に基づいた拡張リファインメント型システムの設計・実装はやや遅れているので、それらに関する取り組みを強化する予定である。
|
| 次年度の研究費の使用計画 |
次年度使用額が生じた主な理由は以下の2つである。
(1)25年度にあげた研究成果の外部発表が25年度中には間に合わなかったため、予定していた旅費と学会参加費がかからなかった
(2)研究補助のための大学院生を確保できなかったため、25年度に予定していた人件費がかからなかった
次年度使用額は以下のように使用する予定である。
(1)25年度にあげた研究成果の外部発表を行い、そのための旅費および学会参加費として使用する
(2)本研究代表者が25年度に卒業論文研究指導を行った2人の現M1学生と、25年度から修士論文研究指導を行っている1人の現M2学生の計3人に本研究を補助してもらい、その人件費として使用する
|
