「一般的な言語 対 ドメイン特化言語」、「上流での実装詳細の捨象の程度」など、記述方式の特化性はソフトウェア開発における難しい問題です。本論文は、フレームワークを用いた開発における形式仕様記述の活用に関し、この問題について様々な観点からの試行と議論を試みています。

概要：

あいまいな仕様による不具合を解決する方法の1つとして形式手法がある。これを、Webアプリケーションのフレームワークを用いた開発に適用する際の課題や問題点を、ケーススタディを通して明らかにする。また、形式記述言語VDM++[1]をいかに活用していくべきかを議論した結果を報告する。