2015 Fiscal Year Annual Research 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. リファインメント型最適化：従来のリファインメント型推論問題を、多目的最適化問題として一般化したリファインメント型最適化問題を提案し、実際にそのような最適化問題を解くための、ホーン節制約最適化に基づく新手法を開発した。これによって、高レベルプログラムの、実行が停止しない入力条件の推論や、最悪の計算ステップ数を引き起こす入力条件の推論といった新しい応用が可能になった。
2. 完全正当性検証：部分正当性に加えて停止性を検証可能なようにリファインメント型システムを拡張し、その型推論問題を整礎性制約付きのホーン節制約解消問題に帰着・解消する手法を提案した。
3. 再帰データ構造の検証：再帰データ構造を扱うプログラムの部分正当性・完全正当性検証を可能とするための拡張を、リファインメント型システムと型推論法に対して行った。
|
Research Products
(8 results)
