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

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

• A.2.3 囚人の割り当て
  • 刑務所で異なるギャングのメンバーを同じ監房に入れないようにする
    • 問題には書いてありませんが、空っぽの Cell(監房)が表示されも無意味なので fact で全ての Cell には誰かが割り当てられているものとしています。またこれも書かれていませんが、テンプレートのモデルだと、ひとりの囚人が複数のギャングに所属することができるようになっているので、これも1つのギャングにのみ所属できるように制約を加えました(問題の意図とは違うかも)

fact {
  // 全ての監房に少なくとも1人は割り当てられる
  all c: Cell | c in Inmate.room
  // 囚人が所属できるギャングは1つだけ
  all i: Inmate | lone members.i
  }

• • (a) 安全な割り当てを表現する述語 safe

pred safe () {
  all i1, i2: Inmate |
    i1.room = i2.room =>
      no members.i1 or no members.i2 or members.i1 == members.i2
  }

• • (b) ギャングメンバーは同じギャングのメンバーとだけ監房を共有する happy という述語を記述してチェック。どのギャングのメンバーでもない囚人と一緒になると happy ではないから

pred happy() {
  all i1, i2: Inmate |
    i1.room = i2.room =>
      members.i1 == members.i2
  }
assert SafeImplyHappy {
  safe => happy
  }
check SafeImplyHappy

• • (c) 安全性(safe)が幸せ(happy)を含意することを保証するような制約を fact で追加
    • 囚人が全員ギャングのメンバーであればいい。他にもあるかな？しかしいやな制約だ……

fact AllInmateAreGangMember {
  all i: Inmate | i in Gang.members
  }

A.2 が終わりました。 付録A は A.1 が長かったのでこれで半分くらいですね。まだ半分というべきか。