情報処理学会 第78回全国大会講演要旨

形式仕様記述は、形式仕様記述言語で仕様を記述することで、仕様の誤りの自動検証を可能にする。既存ツールを用いて形式仕様記述言語VDM++で記述された仕様からプログラミング言語のコードを生成できるが、JavaとC++にしか対応しておらず、また操作の事後条件は無視される等の制約がある。本研究では、VDM++仕様からC#コードを生成するツールの開発を目指す。VDM++記述の検証後に、このツールを用いてVDM++仕様中の事前条件、事後条件および不変条件を生成コード中の契約に変換し、C#から利用できるCode Contractsによる契約情報に基づく実装コードのテストを実施することで，事前・事後・不変条件に基づく検証をシームレスに実現できる。