2015 Fiscal Year Annual Research Report
| Project/Area Number |
25330096
|
|---|
| Research Institution | Tsurumi University |
|---|
Principal Investigator |
田辺 良則 鶴見大学, 文学部, 教授 (60443199)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
山本 光晴 千葉大学, 大学院理学研究科, 准教授 (00291295)
萩谷 昌己 東京大学, 大学院情報理工学系研究科, 教授 (30156252)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | ソフトウェア検証 / 定理証明支援系 / ディペンダブル・コンピューティング |
|---|
| Outline of Annual Research Achievements |
平成28年度は，前年度までに作成したScalaコード生成プログラムをベースに，副作用を持つモジュールに対しても，検証済みコードを作成できるように拡張する方式に関する研究を行った．
対象コードがOCamlである場合には，すでに，Ynotと呼ばれるシステムが作成されている．Ynotでは，副作用を持つ関数はモナドを用いて作成する．事前条件および事後条件を，separation logicによって記述する．Ynotの現行版はCoqの現行版では動作しないので，対象コードをScalaに対して適用するために，Coqに追随するための変更を行った．この作業を通して，Ynotが定義しているtacticsが多数あり，大きな工数が必要となることがわかった．技術的な問題であるため，今回のプロジェクトにおいては完全な追随は行わず，回避手段を用いた．次に，カウンタとスタックを用いて減算式を評価することを例題として定め，試験適用を行った結果，モデル記述についても，Ynotの例題ではとりあげられていない機能で，そのままでは動作しないものがあることがわかり，対応する変更を行った．
このように，Scalaの副作用を持つモジュールの検証に向けた道筋を立てることができた．今後は，上記の技術的な問題点の解消を図りつつ，実装を進めていく予定である．
また，以上に述べたアクティビティを通して得られた知見を，以下の項目を含むCoqコードの開発において応用することができた．(a) ソフトウェアモデル検査を不具合発見に応用するために開発したアルゴリズムの部分検証．(b) ペトリネットの被覆性判定に用いられるKarp-Miller木構成関数の停止性証明．
|
