抽象によるソフトウェア設計 付録A 練習問題 その12

付録A 練習問題まだまだ続きます。

  • A.2.2 アドレス帳の不変条件を保存する
    • (a) 不変条件の述語 inv について説明せよ
      • 「Book b においてすべての Name はそれ自身から addr でたどれるない。つまり addr で循環する関係は存在しない。また addr に存在する Name には少なくとも 1つは Addr に辿りつく関係が addr 内に存在する」
    • (b) 以下のような述語とコマンドで確認
pred SatisfyInv {
  some b: Book | inv [b]
}
run SatisfyInv for 3 but 1 Book
pred NotSatisfyInv {
  some b: Book | not inv [b]
  }
run NotSatisfyInv for 3 but 1 Book
    • (c) add と del のそれぞれについて述語を追加。ただし後の確認のために変更前の Book が inv を満たしていることを制約として入れています
pred AddAddress {
  some b, b': Book | some n: Name | some t: Name + Addr |
    inv [b] and add [b, b', n, t]
  }
run AddAddress for 3 but 2 Book

pred DelAddress {
  some b, b': Book | some n: Name | some t: Name + Addr |
    inv [b] and add [b, b', n, t]
  }
run DelAddress for 3 but 2 Book
    • (d) 以下のような assert で add/del が不変条件を壊すことを確認できる
assert AddKeepInv {
  all b, b': Book | all n: Name | all t: Name + Addr |
    inv [b] and add [b, b', n, t] => inv [b']
  }
check AddKeepInv for 3 but 2 Book

assert DelKeepInv {
  all b, b': Book | all n: Name | all t: Name + Addr |
    inv [b] and del[b, b', n, t] => inv [b']
  }
check DelKeepInv
    • (e) 不変条件が保存されるように述語 add, del を書き換え
pred add (b, b': Book, n: Name, t: Name + Addr) {
  t in Addr or some lookup [b, t]
  not (n in t.^(b.addr) or n = t)
  b'.addr = b.addr + n -> t
  }
pred del (b, b': Book, n: Name, t: Name + Addr) {
  no b.addr.n or some n.(b.addr) - t
  b'.addr = b.addr - n -> t
  }