Toccata

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

   Challenge 2
*)

module MaximumTree

  use int.Int
  use int.MinMax

  type tree = Empty | Node tree int tree

  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

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

  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
      | Empty              -> absurd
      | Node Empty v Empty -> v
      | Node Empty v s
      | Node s     v Empty -> max (maximum s) v
      | Node l     v r     -> max (maximum l) (max v (maximum r))
    end

end