Same fringe
``Same fringe'' is a famous problem. Given two binary search trees, we must decide whether they contain the same elements (more details here).
The solution presented here uses two zippers, to traverse both trees simultaneously. Each zipper corresponds to the left spine of a tree, as a bottom-up list.
Authors: Jean-Christophe Filliâtre
Topics: Trees
Tools: Why3
see also the index (by topic, by tool, by reference, by year)
(* ``Same fringe'' is a famous problem. Given two binary search trees, you must decide whether they contain the same elements. See for instance http://www.c2.com/cgi/wiki?SameFringeProblem *) module SameFringe use int.Int use list.List use list.Length use list.Append (* binary trees with elements at the nodes *) type elt val eq (x y: elt) : bool ensures { result <-> x=y } type tree = | Empty | Node tree elt tree function elements (t : tree) : list elt = match t with | Empty -> Nil | Node l x r -> elements l ++ Cons x (elements r) end (* the left spine of a tree, as a bottom-up list *) type enum = | Done | Next elt tree enum function enum_elements (e : enum) : list elt = match e with | Done -> Nil | Next x r e -> Cons x (elements r ++ enum_elements e) end (* the enum of a tree [t], prepended to a given enum [e] *) let rec enum t e variant { t } ensures { enum_elements result = elements t ++ enum_elements e } = match t with | Empty -> e | Node l x r -> enum l (Next x r e) end let rec eq_enum e1 e2 variant { length (enum_elements e1) } ensures { result=True <-> enum_elements e1 = enum_elements e2 } = match e1, e2 with | Done, Done -> True | Next x1 r1 e1, Next x2 r2 e2 -> eq x1 x2 && eq_enum (enum r1 e1) (enum r2 e2) | _ -> False end let same_fringe t1 t2 ensures { result=True <-> elements t1 = elements t2 } = eq_enum (enum t1 Done) (enum t2 Done) let test1 () = enum Empty Done let test2 () = eq_enum Done Done let test3 () = same_fringe Empty Empty val constant a : elt val constant b : elt let leaf x = Node Empty x Empty let test4 () = same_fringe (Node (leaf a) b Empty) (Node Empty a (leaf b)) let test5 () = same_fringe (Node (leaf a) b Empty) (Node Empty b (leaf a)) exception BenchFailure let bench () raises { BenchFailure -> true } = if not (test4 ()) then raise BenchFailure end module Test use int.Int clone SameFringe with type elt = int let test1 () = enum Empty Done let test2 () = eq_enum Done Done let test3 () = same_fringe Empty Empty constant a : int = 1 constant b : int = 2 let leaf x = Node Empty x Empty let test4 () = same_fringe (Node (leaf a) b Empty) (Node Empty a (leaf b)) let test5 () = same_fringe (Node (leaf a) b Empty) (Node Empty b (leaf a)) end
download ZIP archive