| 研究課題/領域番号 |
25280024
|
|---|
| 研究種目 |
基盤研究(B)
|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
|
|---|
| 研究分担者 |
中澤 巧爾 京都大学, 情報学研究科, 助教 (80362581)
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
馬谷 誠二 京都大学, 情報学研究科, 助教 (40378831)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| キーワード | プログラミング言語 / ソフトウェア契約 / 計算効果 / プログラム検証 / ゲーム意味論 |
|---|
| 研究概要 |
本年度は(1)計算効果を持つ言語機構とソフトウェア契約の統合、(2)ハイブリッド契約検査技術の発展、(3)ソフトウェア契約の代数的意味論の確立についての研究を行った。それぞれについて研究実績を述べる。
(1)計算効果を持つ言語機構として限定継続を取り上げ、動的契約検査の方式の設計および意味論の検討を行った。検査方式は、Danvy と Fillinski のアンサー型の変更を許す型システムにヒントを得て、関数に対する契約を、契約の四つ組として与えることとした。この方式をラムダ計算上でモデル化するために操作的意味論を検討し、その定義を与えた。ただし、契約違反の際にどのモジュールに責任があるかを定めるblameアルゴリズムについて検討課題が残った。
(2)新しいハイブリッド契約検査技術として、代数的データ型に対するハイブリッド契約検査の基礎となる計算体系について研究を行った。代数的データ型に対する契約は、データ型の値を入力として真偽値を返す関数で記述する方法と、Coqなどに代表される、コンストラクタに契約を与えることで記述する方法があるが、それらのふたつの方法の利害得失について考察するとともに、前者の方法で記述された契約を後者の方法に変換する手法を考案し、その正当性について形式体系の上で証明した。また、OCaml用のプリプロセッサCamlP4を用い、形式体系のプロトタイプ実装を行った。
(3)契約計算に対する新しい意味論として、トレース意味論を検討した。トレース意味論は、並行計算などにも見られるが、プログラム部品と環境との相互作用の系列を意味として与えるもので、ゲーム意味論とも関連が深い。具体的には、Findler--Felleisenによる契約計算に対するトレース意味論の定義を与えた。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
研究実績の概要で述べた3つの課題について、交付申請書の段階では想定していなかった課題も浮かびあがったが、いずれも克服の目処がたっている。(3)のゲーム意味論については、トレース意味論の定義だけでなく性質の証明の検討まで入る予定であったが、そこまでは進んでいない。ただし、関連研究調査で Flanagan らの時相契約の枠組が類似のものとして利用可能であることがわかったため、平成26年度にはその研究で行われている証明を一部再利用して効率よく進められるものと考えている。
|
| 今後の研究の推進方策 |
現在までおおむね順調に進んでおり、交付申請書・研究実績の概要であげた3課題についての研究をそのまま進めてゆく。特に、それぞれの課題について1人以上の大学院生の研究協力を見込める体制が整ったため、それを梃子にして研究を推進していく。研究計画の変更は特に考えていない。
|
| 次年度の研究費の使用計画 |
年度当初に予定していた海外出張を家庭の事情により中止したためもあるが、基金の特徴を活かして、研究が想定外に進んだ時のことを考え研究費を確保しておいたため。
研究協力者（大学院博士後期課程学生）への謝金、今年度行わなかった分の海外出張などを行う。
|
