| 研究課題/領域番号 |
25280024
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 一部基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
|
|---|
| 研究分担者 |
馬谷 誠二 京都大学, 情報学研究科, 助教 (40378831)
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
中澤 巧爾 名古屋大学, 情報科学研究科, 准教授 (80362581)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2017-03-31
|
| 研究課題ステータス |
完了 (2016年度)
|
| 配分額 *注記 |
18,070千円 (直接経費: 13,900千円、間接経費: 4,170千円)
2015年度: 5,590千円 (直接経費: 4,300千円、間接経費: 1,290千円)
2014年度: 5,590千円 (直接経費: 4,300千円、間接経費: 1,290千円)
2013年度: 6,890千円 (直接経費: 5,300千円、間接経費: 1,590千円)
|
|---|
| キーワード | プログラミング言語 / ソフトウェア契約 / 計算効果 / プログラム検証 / トレース意味論 / 代入 / 限定継続 / ゲーム意味論 / shift/reset |
|---|
| 研究成果の概要 |
計算効果を持つ言語機構とソフトウェア契約の統合について，FindlerとFelleisenの契約計算やBlame計算の限定継続機構による拡張を行い，動的契約検査のアルゴリズムの形式化やBlame計算としての諸性質の証明を与えた．また，顕在的契約計算の代入機構による拡張を形式化し，その諸性質を示した．代数的データ型による顕在的契約計算を提案し，その上で，代数的データ型に対する契約記述のふたつの方法について比較し，一方から他方へは変換が可能であること示した．また，この計算体系の実装として OCaml 処理系の拡張を行った．ソフトウェア契約の代数的意味論としてトレース意味論を研究した．
|
