foveoos11_challenge2.mlw 903 Bytes
 Jean-Christophe Filliatre committed Oct 05, 2011 1 2 3 4 5 6 7 8 9 `````` (* FoVeOOS 2011 verification competition http://foveoos2011.cost-ic0701.org/verification-competition Challenge 2 *) module MaximumTree `````` Andrei Paskevich committed Jun 15, 2018 10 11 `````` use int.Int use int.MinMax `````` Jean-Christophe Filliatre committed Oct 05, 2011 12 13 14 `````` type tree = Empty | Node tree int tree `````` Jean-Christophe Filliatre committed Oct 12, 2011 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 `````` Jean-Christophe Filliatre committed Oct 05, 2011 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 `````` Andrei Paskevich committed Oct 13, 2012 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 `````` Jean-Christophe Filliatre committed Oct 08, 2011 31 `````` | Empty -> absurd `````` Jean-Christophe Filliatre committed Oct 05, 2011 32 `````` | Node Empty v Empty -> v `````` Jean-Christophe Filliatre committed Oct 08, 2011 33 34 `````` | Node Empty v s | Node s v Empty -> max (maximum s) v `````` Jean-Christophe Filliatre committed Oct 05, 2011 35 36 37 38 `````` | Node l v r -> max (maximum l) (max v (maximum r)) end end``````