抽象によるソフトウェア設計 付録A 練習問題 その12
付録A 練習問題まだまだ続きます。
- A.2.2 アドレス帳の不変条件を保存する
- (a) 不変条件の述語 inv について説明せよ
- 「Book b においてすべての Name はそれ自身から addr でたどれるない。つまり addr で循環する関係は存在しない。また addr に存在する Name には少なくとも 1つは Addr に辿りつく関係が addr 内に存在する」
- (b) 以下のような述語とコマンドで確認
- (a) 不変条件の述語 inv について説明せよ
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 }