examples/foveoos11_challenge2.mlw

   1
   2 (* FoVeOOS 2011 verification competition
   3    http://foveoos2011.cost-ic0701.org/verification-competition
   4
   5    Challenge 2
   6 *)
   7
   8 module MaximumTree
   9
  10   use int.Int
  11   use int.MinMax
  12
  13   type tree = Empty | Node tree int tree
  14
  15   function size (t: tree) : int = match t with
  16     | Empty      -> 0
  17     | Node l _ r -> 1 + size l + size r
  18   end
  19
  20   lemma size_nonneg: forall t: tree. size t >= 0
  21
  22   predicate mem (x: int) (t: tree) = match t with
  23     | Empty      -> false
  24     | Node l v r -> mem x l \/ x = v \/ mem x r
  25   end
  26
  27   let rec maximum (t: tree) : int variant { size t }
  28     requires { t <> Empty }
  29     ensures { mem result t /\ forall x: int. mem x t -> x <= result }
  30   = match t with
  31       | Empty              -> absurd
  32       | Node Empty v Empty -> v
  33       | Node Empty v s
  34       | Node s     v Empty -> max (maximum s) v
  35       | Node l     v r     -> max (maximum l) (max v (maximum r))
  36     end
  37
  38 end