実行可能形式仕様記述言語VDM-SLの実行を主目的とするバーチャルマシンを、データモデル、メモリモデル、レジスタモデル、バイトコードのインストラクションセット、実行コンテキスト(アクティベーション・レコード)およびコード領域の形式仕様をVDM-SLにより記述し、C言語による実装でx64プロセッサおよびarm32およびarm64プロセッサの3種類のプロセッサ向けにビルドし、実行させた。VDM-SL仕様とC実装の両方に同じユニットテストを適用することで、C言語のユニットテストでのエラーの原因が仕様レベルであるか実装レベルであるかを容易に判別することができ、C言語による実装の生産性が良好だった。
|