形式手法を俯瞰する
参考
『形式手法入門』.icon p.10で参照されてる148
形式手法の分野では3つの分野がある
ただし、3つは排他的なものではない
ツールに依っては複合しているものもある
形式手法の検証方法
モデル中の仕様に矛盾がないことを数学的に証明する
証明すべき論理式を書くには相応の知識が必要
自動生成できる場合もある
仕様の修正があると証明を書き直す必要がある
形式手法
ソフトウェアの多種多様な正しさを記述できるが、プログラマ側に高度な知識を要求する
ex.
軽量形式手法
理論に馴染みのないプログラマでも使用でき、コンパイラやリンカに埋め込むことができるもの
ex.
↑の分類がわからないやつ
形式仕様言語の分類 ref 『形式手法入門』.icon p.10
記述の要素が持つ意味(構文上の要素)を、数学的な実体(意味モデル)集合、関係、列、関数などに対応させる
意味がわからんmrsekut.icon
記述の要素(構文上の要素)が満たす関係式を定義することで、要素の意味を与える
代数を用いてデータ型やプロセスを定義する代数仕様
述語論理を元にした公理的な方法
実際はこんな風に明確に2分類されるわけでもない
1つの言語が複数のアプローチを使えることもある
どのような観点から対象を記述するかという分類 ref 『形式手法入門』.icon p.10
履歴に基づく仕様
実行経路の集まりからなるふるまいの仕様の取り扱いを目的とする
状態に基づく仕様
VDM, Bメソッド
状態遷移仕様
オートマトン
SPIN
関数的な仕様
数学的な関数によって表現
操作的な仕様