| 大会名称 |
|---|
| 2018年 情報科学技術フォーラム(FIT) |
| 大会コ－ド |
| F |
| 開催年 |
| 2018 |
| 発行日 |
| 2018-09-12 |
| セッション番号 |
| 2b |
| セッション名 |
| ソフトウェア（２） |
| 講演日 |
| 2018/09/19 |
| 講演場所(会議室等) |
| C棟C33 |
| 講演番号 |
| IA-002 |
| タイトル |
| Stateful Manifest Contracts |
| 著者名 |
| 関山太朗, 五十嵐淳, |
| キーワード |
| 型システム, ソフトウェア契約, ハイブリッド検査 |
| 抄録 |
| 本講演では顕在的契約計算に命令型プログラミングの基本機能であるプログラム状態変化（メモリ操作）機構を導入した研究について発表する。顕在的契約計算ではプログラムの仕様をプログラミング言語で記述した述語を篩（ふるい）型と呼ばれる型に与えることで表現し、プログラムが篩型の仕様を満たすかは静的または実行時検査する。プログラムの状態に依存した述語を許すために、本研究ではNanevskiらのホーア型を取り入れた顕在的契約計算を新たに設計、さらに状態変更を伴うような仕様として不適切な述語を検知するためにリージョンに基づく効果システムを導入し、我々の顕在的契約計算の健全性を証明した。 |
| 本文pdf |
| PDF download (181.1KB) |