2014 Fiscal Year Annual Research Report
検証技術と非標準型体系を用いたモデル検査器コンパイラの進化的発展
| Project/Area Number |
24650016
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
上田 和紀 早稲田大学, 理工学術院, 教授 (10257206)
|
|---|
| Project Period (FY) |
2012-04-01 – 2015-03-31
|
| Keywords | モデル検査 / コンパイラ / 検証 / 型体系 / ソフトウェア進化 |
|---|
| Outline of Annual Research Achievements |
階層グラフ書換えに基づくモデリング言語LMNtalのコンパイラの進化およびグラフ書換えの記述力の強化を目指し，以下の研究開発を進めた．
1. LMNtalの書換え規則は，マッチすべき部分グラフを具体的に指定するか，連結グラフなどあらかじめ定められた一定の性質を満たす部分グラフを包括的に指定することを許していたが，部分グラフの族を利用者が自由に定義することはできなかった．そこで，グラフの集合を表現するための再帰的な生成文法を設計し，グラフの持つべきパターンによって簡約基を指定できる処理系をGaucheで実装した．実装にあたって，パターンマッチングのメモ化が多くの例題で計算量を改善することを確認した．パターン記述言語の表現力の確認のために，評価文脈を用いたプログラミング言語の操作的意味論や一級継続の意味論をグラフ書換え系として記述し，実行することに成功した．
2. グラフ構造を扱う型体系であるShape TypeをLMNtalに導入した．グラフが特定の構造を持っているかどうかの検査（グラフの型検査）および書換え規則がその構造を崩さないかどうかの検査（ルールの型検査）の概念を定め，前者に関してはアルゴリズムを提示し，その停止性と健全性の証明を与えた．グラフやルールの型検査がグラフ書換えを用いた探索に帰着でき，LMNtalプログラムの非決定的な実行を探索に利用できることに着目し，既存のLMNtal処理系を用いて検査を行う手法を実装した．
3. ハイパーリンク機能をもつHyperLMNtalの言語仕様の妥当性評価のために，高階単一化機能をもつ高階論理型言語のHyperLMNtalへのエンコーディングを行い動作確認を行った．
また，稼働中のLMNtal処理系への諸研究成果の統合を目指し，コンパイラの整備改良を進めて新たにソースコードをGitHubから公開した．
|
