そもそも形式的手法って何?

形式的な仕様記述は1970年代に欧州で生まれ,代表的な手法に「VDM」「Z」「B」「OCL」「OBJ」などがあります。一方,形式検証は比較的新しく1990年代に実用化されました。モデル検査と呼ぶ手法があり,「SPIN」「SMV」「Uppaal」などのツールが無償で公開されています。

形式検証って,確かLSI設計の話では?ソフトにも関係するの?

モデル検査の教科書の表紙には,回路基板の上に虫(バグ)が乗っている絵柄が使われている。

関係があります。形式的手法は,もともとはソフトウエア開発のために生まれました。ただし,形式的手法の一種である形式検証については,先にLSI設計向けに実用化されたために,そうしたイメージがあるようです。日本国内でも,LSI設計者であれば「フォーマル・ベリファイア」というツール名で聞き覚えがある状況です。

形式的な仕様記述言語ってプログラミング言語とは何が違うの?

記述する内容にもよりますが,見た目はそれほど大きく違いはありません。記述できる内容についても重複があります。例えば,四則演算や条件判断などのプログラミング構文は,形式的な仕様記述言語にもプログラミング言語にもあります。プログラミング言語にはない要素で,形式的な仕様記述言語を特徴付けているのは,関数が実行される前はこういう状態(事前条件),関数が実行された後はこうなっていなければならない(事後条件),といったソフトウエアの仕様を明示的に書けることです。

形式的手法とプログラミング言語との比較表
[画像のクリックで拡大表示]

この先は会員の登録が必要です。今なら有料会員(月額プラン)が12月末まで無料!