2015 Fiscal Year Annual Research Report
| Project/Area Number |
25280024
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
馬谷 誠二 京都大学, 情報学研究科, 助教 (40378831)
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
中澤 巧爾 名古屋大学, 情報科学研究科, 准教授 (80362581)
|
|---|
| Project Period (FY) |
2013-04-01 – 2017-03-31
|
| Keywords | プログラミング言語 / ソフトウェア契約 / 計算効果 / プログラム検証 / ゲーム意味論 / shift/reset |
|---|
| Outline of Annual Research Achievements |
今年度設定した3つの研究課題: (1) 計算効果を持つ言語機構とソフトウェア契約の統合，(2) ハイブリッド契約検査技術の代数的データ型への適用，(3) ソフトウェア契約の代数的意味論の確立について取り組み，以下のような成果をあげた．
(1) 計算効果を持つ言語機構とソフトウェア契約の統合: 様々な計算効果を表現できることが知られている限定継続機構 shift/reset に対して，静的型システムと動的型システムを統合したような検査機構を形式化し，その諸性質を証明した．これは
Wadler と Findler による blame calculus の拡張になっている．また諸性質として型健全性だけでなく，動的検査失敗時のエラー (blame) の正しさを示す blame theorem や，blame calculus の CPS 変換とその健全性などを示すことができた．
(2) 当初の予定では，ユーザ定義型のためのキャストのコスト削減手法に取組むことになっていたが，プロトタイプ実装の完成度を高め，コスト評価に関する実験などができる環境を整えることになった．そのために，OCaml の型推論とハイブリッド契約機構の融合に取組んだ．結果として，型を省いた契約情報つきのプログラムから，型情報を OCaml と類似の型推論技法により回復するとともに適当なキャストを挿入するための型推論アルゴリズムを構築し，その健全性を示した．
(3) 昨年度までに，単純型付ラムダ計算に単純な契約を付加した体系に対するトレース意味論を構築し,それが操作的意味論と対応していることや,文脈等価性に対して健全かつ完全であることの証明を行っていたが，その内容を精査する過程で計算体系の定義や証明に細かなミスが多数見つかったために，今年度は体系定義の見直し・簡略化とミスの除去を行った．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
(1) の計算効果を持つ言語機構とソフトウェア契約の統合については，当初の計画通り，blame theorem の形で，契約違反の直観を形式化・正当性を示すことができただけでなく，blame calculus の CPS 変換の研究などは計画を越えて研究が進展した．
(2) については，年度当初に設定した研究課題から方向性を変更した部分があるが，変更した方向では順調に進展した．
(3) は，前年度までの成果の中の細かなミスによって年度当初に設定した研究課題通りに進まなかった部分もある．
以上のように研究課題によって進展具合に差があるが全体的にはおおむね順調したと考えている．
|
| Strategy for Future Research Activity |
(3)については，ミスを修正した上でその成果を発表すべく，繰越しを行った．また，(2)については，引き続き博士課程学生の研究として続行する予定である．
|
| Causes of Carryover |
研究成果の一部である、契約計算の新しい意味論についての結果を国際会議で発表することを計画していたが、理論の大枠は完成したものの、一部の定理の証明に誤りがあることがわかったため、その修正を行った上で平成28年度中に成果発表を行う。
|
| Expenditure Plan for Carryover Budget |
論文成果発表のための旅費と国際会議参加費に使用する予定である。
|
