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

今日は 5.3 非限定の全称限量子からです。実は昨日もここを読んでいたのですが、読み解くのが難しくて昨日はメモを書けなかったのでした。

• 生成公理とスコープの爆発
  • 集合を表すシグネチャ Set の論理和についての検査を書く

sig Element {}
sig Seg { elements: set Element }
assert Closed {
  all s0, s1 : Set | some s2: Set |
    s2.elements = s0.elements + s1.elements

• • これをスコープ 3 で検査すると s2 に相当する値を生成しない例を検出してしまう
  • 「生成公理」を導入して必ず必要な集合が生成されることを要請する
    • 帰納法的に、Elements の組み合わせの全ての集合が必ず生成されることを制約として書く

fact SetGenerator {
  some s: Set | no s.elements
  all s:Set, e: Element |
    some s': Set | s'.elements = s.elements + e
  }

• • これで assert は通るようになるけど、Element のスコープに対して Set のスコープが 2^n 必要になる
  • グラフ構造やリスト構造ではもっと多く、または無限のスコープが必要になってしまう → スコープの爆発
• 実は assert の限量子の使いかたを変えた記述方法にすれば生成公理を導入せずにすむ

assert UnionCommutative {
  all s0, s1, s2: Set |
    s0.elements + s1.elements = s2.elements
    implies s1.elements + s0.elements = s2.elements

• • この記述方法だと assert の検査のために否定した時に全称限量子がなくなって偽反例が検出されない
• 「限定全称限量子」だけを使うようにすればOK

難しいですね。まだ限定全称限量子だけを使うようにする方法はピンときていませんが、とにかく否定した時に全称限量子が残っているとまずいというとですね。