examples/same_fringe.mlw

   1
   2 (*
   3   ``Same fringe'' is a famous problem.
   4   Given two binary search trees, you must decide whether they contain the
   5   same elements. See for instance http://www.c2.com/cgi/wiki?SameFringeProblem
   6 *)
   7
   8 module SameFringe
   9
  10   use int.Int
  11   use list.List
  12   use list.Length
  13   use list.Append
  14
  15   (* binary trees with elements at the nodes *)
  16
  17   type elt
  18
  19   val eq (x y: elt) : bool ensures { result <-> x=y }
  20
  21   type tree =
  22     | Empty
  23     | Node tree elt tree
  24
  25   function elements (t : tree) : list elt = match t with
  26     | Empty -> Nil
  27     | Node l x r -> elements l ++ Cons x (elements r)
  28   end
  29
  30   (* the left spine of a tree, as a bottom-up list *)
  31
  32   type enum =
  33     | Done
  34     | Next elt tree enum
  35
  36   function enum_elements (e : enum) : list elt = match e with
  37     | Done -> Nil
  38     | Next x r e -> Cons x (elements r ++ enum_elements e)
  39   end
  40
  41   (* the enum of a tree [t], prepended to a given enum [e] *)
  42
  43   let rec enum t e variant { t }
  44     ensures { enum_elements result = elements t ++ enum_elements e }
  45   = match t with
  46     | Empty -> e
  47     | Node l x r -> enum l (Next x r e)
  48     end
  49
  50   let rec eq_enum e1 e2 variant { length (enum_elements e1) }
  51     ensures { result=True <-> enum_elements e1 = enum_elements e2 }
  52   = match e1, e2 with
  53     | Done, Done ->
  54         True
  55     | Next x1 r1 e1, Next x2 r2 e2 ->
  56         eq x1 x2 && eq_enum (enum r1 e1) (enum r2 e2)
  57     | _ ->
  58         False
  59     end
  60
  61   let same_fringe t1 t2
  62     ensures { result=True <-> elements t1 = elements t2 }
  63   = eq_enum (enum t1 Done) (enum t2 Done)
  64
  65   let test1 () = enum Empty Done
  66   let test2 () = eq_enum Done Done
  67   let test3 () = same_fringe Empty Empty
  68
  69   val constant a : elt
  70   val constant b : elt
  71
  72   let leaf x = Node Empty x Empty
  73
  74   let test4 () = same_fringe (Node (leaf a) b Empty) (Node Empty a (leaf b))
  75   let test5 () = same_fringe (Node (leaf a) b Empty) (Node Empty b (leaf a))
  76
  77   exception BenchFailure
  78
  79   let bench () raises { BenchFailure -> true } =
  80     if not (test4 ()) then raise BenchFailure
  81
  82 end
  83
  84 module Test
  85
  86   use int.Int
  87   clone SameFringe with type elt = int
  88
  89   let test1 () = enum Empty Done
  90   let test2 () = eq_enum Done Done
  91   let test3 () = same_fringe Empty Empty
  92
  93   constant a : int = 1
  94   constant b : int = 2
  95
  96   let leaf x = Node Empty x Empty
  97
  98   let test4 () = same_fringe (Node (leaf a) b Empty) (Node Empty a (leaf b))
  99   let test5 () = same_fringe (Node (leaf a) b Empty) (Node Empty b (leaf a))
 100
 101 end