抽象によるソフトウェア設計 第5章 解析 その1

抽象によるソフトウェア設計−Alloyではじめる形式手法−

今日から第5章に入ります。 Alloy を使ってモデルを作る目的がこの解析にあるはずなので、どんなことが可能なのか知りたいと思います。

• スコープ(要素数の範囲)内で充足例や反例を探す
  • 述語(pred)のシミュレーション(充足例を探し表示する)とアサーション(assert)の検査(反例を探す)は同じことなのでここではアサーションについてのみ記述する
• Alloy の関係論理は決定不能=あるassertが正しいことを完璧な信頼性で答えることはできない
  • 従来の妥協策は「定理証明」
    • 証明に成功すれば assert は正しいが、失敗すると「正しいかどうかわからない」としかわからない
  • Alloy の方針は「インスタンス発見」 反駁(refutation)を探す
    • 反例がみつかれば assert は間違っているが、みつからなくても絶対正しいとはわからない(もっとインスタンス数の多いスコープに反例があるかもしれない)
• スコープ - 各シグネチャの要素数の上限
  • 小スコープ仮説 - ほとんどのバグは小さな反例を持つ。つまり小さいスコープを網羅すればたいていの不具合はみつかる
    • とはいえ適切な assert が書かれていた時だけ……
• 解析の目的は不具合の早期検出というよりも、モデルの構築(つまり設計)を補助しきれいな設計に導くこと。TDD の思想にも似ているような
• 経時変化は(本書では)時間から状態への関数としてモデル化している。解析器にとってはあくまでフィールドのひとつとして時刻があるだけ
• 解析器は制約をブール式に変換して SAT ソルバで解く(高速に解ける)
• スコーレム化
  • 関係式に限量子が含まれる場合に、限量子を展開してしまうかわりに自由変数(スコーレム定数)を導入する形式に変換する
  • some x : S | F => (sx: S) and F [sx/x]
  • これにより反例はその具体的なインスタンスの束縛(証拠 witness)を含む