2016 Fiscal Year Annual Research Report
Theory of Higher-Order Typed Programs based Software Contracts
| 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 | プログラミング言語 / ソフトウェア契約 / 計算効果 / プログラム検証 / トレース意味論 / 代入 |
|---|
| Outline of Annual Research Achievements |
平成27年度に設定した3つの研究課題 (1) 計算効果を持つ言語機構とソフトウェア契約の統合,(2) ハイブリッド契約検査技術の代数的データ型への適用, (3) ソフトウェア契約の代数的意味論の確立について，主に(3)で技術的困難が生じていたために研究期間の延長を行った．
しかし，(3)として行った契約計算体系の定義の修正は完了せず研究発表を行うまでに至らなかった．操作的意味論とトレース意味論というふたつの意味論の間である種の等価性を示すのが目標のひとつとなるが，両者が整合するようにそれぞれの定義を与えるのが困難であるのに起因している．本補助金終了後もこの問題に取り組んでいく予定である．
一方，(3)とは並行して平成27年度研究課題の続きの研究について以下の成果があがった．(1) について，従来の顕在的契約計算に計算効果の代表的なものである代入機構を導入し，形式的計算体系を与え，その型健全性を示すことに成功した．本研究で考えているソフトウェア契約の枠組みにおいては，プログラムの仕様をプログラム記述のための言語で書くので，その言語に代入など状態を変化させる機能と素朴に組み合わせると，プログラムの仕様が状態に依存してしまったり，仕様記述を実行するとプログラム状態を変更してしまう，という問題があった．本研究では，プログラムで代入を使う箇所と使わない箇所を切りわけることでその問題を解決した．また，代入を使用する部分の契約記述の新しい手法を既存のホーア型と呼ばれる機構を修正し組み込んだ．
|
| Research Progress Status |
28年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
28年度が最終年度であるため、記入しない。
|
-
-
-
-
-
-
[Presentation] Stateful manifest contracts2017
Author(s)
Taro Sekiyama, Atsushi Igarashi
Organizer
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)
Place of Presentation
フランス・パリ
Year and Date
2017-01-18 – 2017-01-20
Int'l Joint Research
-
-
-
