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

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

A.1.10 アドレス帳の制約と式
- まず不変条件を記述

abstract sig Name {
  address: set Addr + Name
  }
sig Alias, Group extends Name {}
sig Addr {}

fact {
  -- 循環がないこと(addressの推移閉包に自分が含まれない)
  no n: Name | n in n.^address
  -- すべての名前は最終的にアドレスに対応付けられる
  all n: Name | some n.address
  }

- - 「全ての名前は最終的にアドレスに対応付けられる」は最初もっとややこしく書いていたのですが、1つめの循環の禁止と合わせて考えると、Alias や Group (つまり Name)が必ず address で対応する子を1つ以上もつことを指定すれば結果としていずれ Addr に辿り着くと気がついたので、address が空ではないという制約の書き方にしました。fact に書くくらいなら Name の宣言で多重度に set ではなく some を使えばいいんですけどね
- シミュレーション制約を記述

run {
  -- 少なくとも2レベルの階層を持つ→Nameに対応する名前が少なくとも1つ存在する
  some n: Name | some n.address & Name
  -- いくつかのグループは空ではない(？)
  some g: Group | some g.address
  }

- - 「いくつかのグループは空ではない」という制約は不変条件として導入した「全ての Name は address に1つ以上の子を持つ」というのに含まれているので無意味になっていると思います。どちらかの問題の解釈を間違っているのかも……(でも空のグループ(グループも名前)はアドレスに対応付けられないことになるのでこれで合っているはず)。
- 式の記述

-- グループのメンバーである名前の集合
--   つまり Group の address に含まれる Name
Group.address & Name

-- 空であるグループの集合
none   -- ？？？

-- 別名から(直接、間接的に)参照するアドレスの集合
Alias.^address & Addr

-- 別名からアドレスの対応
-- ただし同じ名前が直接アドレスに対応しているものと
-- 間接的に別のアドレスに対応しているものがあったら直接対応しているほうを優先する

- - 同様に「空であるグループの集合」は内包表記を使わずに書く方法がわからなかったのと、そもそも不変条件から空集合になるはずなのでひっかけ問題？
  - 最後の問題は時間切れ。直接対応する時の集合と間接的に対応するものをそれぞれ式にして、オーバーライド(++)で足し合わせればいいだろうと思います

だんだん難しくなってきて、解答を参照して答えあわせしたくなってきました。本書中にはなさそうなのですが、どこかに解答例は公開されているでしょうか。