抄録
IA-002
Stateful Manifest Contracts
関山太朗(NII)・五十嵐淳(京大)
本講演では顕在的契約計算に命令型プログラミングの基本機能であるプログラム状態変化(メモリ操作)機構を導入した研究について発表する。顕在的契約計算ではプログラムの仕様をプログラミング言語で記述した述語を篩(ふるい)型と呼ばれる型に与えることで表現し、プログラムが篩型の仕様を満たすかは静的または実行時検査する。プログラムの状態に依存した述語を許すために、本研究ではNanevskiらのホーア型を取り入れた顕在的契約計算を新たに設計、さらに状態変更を伴うような仕様として不適切な述語を検知するためにリージョンに基づく効果システムを導入し、我々の顕在的契約計算の健全性を証明した。