Binary Tree
Specification (cont.)
ä Axioms
ä Add(Create, E) = Build(Create, E, Create)
ä Add(B, E) =
     if E < Data(B) then Add(Left(B),E)
               else Add(Right(B),E)
ä Left(Create) = Create
ä Right(Create) = Create
ä Data(Create) = Undefined
ä Left(Build(L,D,R)) = L
ä Right(Build(L,D,R)) = R
ä Data(Build(L,D,R) = D
ä Is_empty(Create) = true
ä Is_empty(Build(L,D,R)) = false
ä Contains(Create,E) = false
ä Contains(Build(L,D,R),E) =
   if E = D then true
                 else if E < D then Contains(L,E)
          else Contains(R,E)