| 研究課題/領域番号 |
25280024
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
|
|---|
| 研究分担者 |
馬谷 誠二 京都大学, 情報学研究科, 助教 (40378831)
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
中澤 巧爾 名古屋大学, 情報科学研究科, 准教授 (80362581)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2017-03-31
|
| キーワード | プログラミング言語 / ソフトウェア契約 / 計算効果 / プログラム検証 / トレース意味論 / 代入 |
|---|
| 研究実績の概要 |
平成27年度に設定した3つの研究課題 (1) 計算効果を持つ言語機構とソフトウェア契約の統合,(2) ハイブリッド契約検査技術の代数的データ型への適用, (3) ソフトウェア契約の代数的意味論の確立について，主に(3)で技術的困難が生じていたために研究期間の延長を行った．
しかし，(3)として行った契約計算体系の定義の修正は完了せず研究発表を行うまでに至らなかった．操作的意味論とトレース意味論というふたつの意味論の間である種の等価性を示すのが目標のひとつとなるが，両者が整合するようにそれぞれの定義を与えるのが困難であるのに起因している．本補助金終了後もこの問題に取り組んでいく予定である．
一方，(3)とは並行して平成27年度研究課題の続きの研究について以下の成果があがった．(1) について，従来の顕在的契約計算に計算効果の代表的なものである代入機構を導入し，形式的計算体系を与え，その型健全性を示すことに成功した．本研究で考えているソフトウェア契約の枠組みにおいては，プログラムの仕様をプログラム記述のための言語で書くので，その言語に代入など状態を変化させる機能と素朴に組み合わせると，プログラムの仕様が状態に依存してしまったり，仕様記述を実行するとプログラム状態を変更してしまう，という問題があった．本研究では，プログラムで代入を使う箇所と使わない箇所を切りわけることでその問題を解決した．また，代入を使用する部分の契約記述の新しい手法を既存のホーア型と呼ばれる機構を修正し組み込んだ．
|
| 現在までの達成度 (段落) |
28年度が最終年度であるため、記入しない。
|
| 今後の研究の推進方策 |
28年度が最終年度であるため、記入しない。
|
