## FoVeOOS'11 Competition: challenge 2 in Why3

Authors: Jean-Christophe Filliâtre

Topics: Trees

Tools: Why3

References: The COST FoVeOOS'11 Competition

see also the index (by topic, by tool, by reference, by year)

(* 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