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

付録A 練習問題続きます。終わるのかなこれ。

• A.1.11 地下鉄をモデリングする
  • 路線 line にある駅の集合が S

abstract sig Station {
  line: set Station
  }

sig S extends Station {} { S = line }

• • line には切れ目がない

run C {
  all disj x, y: S, z: S |
    y in x.^line or x in y.^line and
    z in x.^line or z in y.^line
  }

一応書いてみたんですが、これで合ってる自信がまったくないので明日も同じ問題を見返します。いつ終わるんだろう……。