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

付録A続きます。

• A.1.5 木を特徴付ける
  • 単射的である(親ノードは1つ)というのすぐ出てきたのですが、循環を防ぐための ^ 演算子(推移閉包)を使う書きかたがなかなか出てきませんでした

pred isTree (r: univ -> univ) {
     r.~r in iden  -- 単射的
     no iden & r  -- 非反射的
     no x: univ | univ in x.^r     -- どのノードも子を辿って自分自身に到達しない。つまり循環しない
     -- some x: univ | some x.r.r  -- 深さ3以上の木を作るための制約
  }

• • ノード間の関係rについての制約なのでノード1つだけの木というのはこの場合はない
  • コメントアウトしてある制約は深さが3以上の制約をつけることで木らしいインスタンスを表示させるため

今日は1つだけでタイムアップ。