| 研究課題/領域番号 |
25280024
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
|
|---|
| 研究分担者 |
馬谷 誠二 京都大学, 情報学研究科, 助教 (40378831)
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
中澤 巧爾 京都大学, 情報学研究科, 助教 (80362581)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| キーワード | プログラミング言語 / ソフトウェア契約 / 計算効果 / プログラム検証 / ゲーム意味論 |
|---|
| 研究実績の概要 |
今年度設定した3つの研究課題(1)計算効果を持つ言語機構とソフトウェア契約の統合，(2)ハイブリッド契約検査技術の代数的データ型への適用，(3)ソフトウェア契約の代数的意味論の確立，について取組み，以下のような成果をあげた．
(1) 計算効果を持つ言語機構とソフトウェア契約の統合: 昨年度の研究で構築したshift/resetを使った限定継続機構を導入した契約計算体系の意味論を見直し，まず限定継続機構を除去するCPS変換を定義し，その意味論を引き戻すことで新しい意味論を得た．また，この意味論から導出できるプログラムの等価性がCSP変換を通じて健全であることを証明した．古い意味論にあった，契約違反が生じた時のblameの非自明な部分も，新しい意味論では直観的には理解がしやすいものになっているが，この直観を形式化することがまだ課題として残っている．
(2) ハイブリッド契約検査技術の代数的データ型への適用: 昨年度の研究で構築した代数的データ型に対するハイブリッド契約検査の枠組みについて，プログラミング言語分野で最も権威のある国際会議のひとつである ACM POPLで成果発表を行った．また，今年度計画していた，この枠組みの欠点のひとつであるデータ型間のキャストの際に生じるコンストラクタ変換のコスト削減手法の考案については，まだ，あまり成果がないが，その後予定される本格的な検証実験の準備として，並行して，計算体系の実装をOCamlコンパイラを改造することで進めた．
(3) ソフトウェア契約の代数的意味論の確立: 昨年度までに目処をたてた，単純型付ラムダ計算に単純な契約を付加した体系に対するトレース意味論を構築し，Findler-Felleisen流の契約に対する操作的意味論とある意味で一致することを証明した．また，付加的結果として，この意味論が文脈等価性と呼ばれるプログラム等価性に対し完全抽象的(fully abstract)であるという予想もほぼ証明できている．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
研究実績の概要で述べた3つの課題について、交付申請書で計画した通りに進んでいる．処がたっている。(2)での，データ型間のキャストの際に生じるコンストラクタ変換のコスト削減手法については，具体的な成果がでていないが，検討を進めていく段階で，問題解決には様々なアプローチと付帯的な問題があることがわかったためその利害得失を見極めている段階である．
|
| 今後の研究の推進方策 |
現在までおおむね順調に進んでおり、交付申請書・研究実績の概要であげた3課題についての研究をそのまま進めてゆく。(1)と(2)の課題については1人以上の大学院生の研究協力を見込める体制が整ったため、それを梃子にして研究を推進していく。研究計画の変更は特に考えていない。
|
| 次年度使用額が生じた理由 |
最終年度に契約計算のコンパイラ実装を進めるにあたって、研究者の人件費を確保するため。
|
| 次年度使用額の使用計画 |
平成27年9月博士課程修了者をポスドク研究員として年度後半に雇用することを計画している。
|
