二分探索木をAlloyで定義してみた

binaty_tree.als

open util/ordering[Node]
sig Node {
   lhs : lone Node,
   rhs : lone Node
}

fact {
   // 葉をたどればすべての要素が取得できるrootがただひとつ存在する
   one root : Node | Node = root.*(lhs+rhs)
   // 任意の節において成り立つ
   all n : Node {
      // 左葉と右葉には共通する節が存在しない
      no n.lhs.*(lhs+rhs) & n.rhs.*(lhs+rhs)
      // 節間の葉関係は循環しない
      not n in n.^(lhs+rhs)
      // 葉が存在するなら、それは left < n <= right という関係になる
      one n.lhs => lt [n.lhs, n]
      one n.rhs => lte[n, n.rhs]
   }
}

pred show {}

run show for 10 Node