foveoos11_challenge2.mlw 903 Bytes
Newer Older
1 2 3 4 5 6 7 8 9

(* FoVeOOS 2011 verification competition
   http://foveoos2011.cost-ic0701.org/verification-competition

   Challenge 2
*)

module MaximumTree

10 11
  use int.Int
  use int.MinMax
12 13 14

  type tree = Empty | Node tree int tree

15 16 17 18 19 20 21
  function size (t: tree) : int = match t with
    | Empty      -> 0
    | Node l _ r -> 1 + size l + size r
  end

  lemma size_nonneg: forall t: tree. size t >= 0

22 23 24 25 26
  predicate mem (x: int) (t: tree) = match t with
    | Empty      -> false
    | Node l v r -> mem x l \/ x = v \/ mem x r
  end

27 28 29 30
  let rec maximum (t: tree) : int variant { size t }
    requires { t <> Empty }
    ensures { mem result t /\ forall x: int. mem x t -> x <= result }
  = match t with
31
      | Empty              -> absurd
32
      | Node Empty v Empty -> v
33 34
      | Node Empty v s
      | Node s     v Empty -> max (maximum s) v
35 36 37 38
      | Node l     v r     -> max (maximum l) (max v (maximum r))
    end

end