構造 (Structure ・ Model) の概念の再訪

構造は、議論領域と記号の解釈を組にしたモデルであり、式がどの条件で真になるかを定める。形式仕様のモデルは、現実の全詳細ではなく検証対象を抽象化したものだ。

仕組みと確認

状態・関係・操作をモデルとして明示し、要求がすべての許容状態で成立するか、反例状態が実システムに対応するかを確認する。

限界と注意点

抽象化は検証を可能にする一方、重要な挙動を隠す。モデルの範囲・環境仮定・抽象化の妥当性を成果物として残す。