diff --git a/examples/foveoos2011/tree_max.mlw b/examples/foveoos2011/tree_max.mlw new file mode 100644 index 0000000000000000000000000000000000000000..46347e35ff9b361613355d64befc86031b34f94d --- /dev/null +++ b/examples/foveoos2011/tree_max.mlw @@ -0,0 +1,85 @@ +(* +COST Verification Competition. vladimir@cost-ic0701.org + +Challenge 2: Maximum in a tree + + +Given: A non-empty binary tree, where every node carries an integer. + +Implement and verify a program that computes the maximum of the values +in the tree. + +Please base your program on the following data structure signature: + +public class Tree { + + int value; + Tree left; + Tree right; + +} + +You may represent empty trees as null references or as you consider +appropriate. +*) + +theory BinTree + + use import int.Int + use import int.MinMax + + type tree = Null | Tree int tree tree + + (* tests whether an integer v occurs in t *) + predicate mem (v:int) (t:tree) = + match t with + | Null -> false + | Tree x l r -> x=v \/ mem v l \/ mem v r + end + + (* tests whether an integer is greater or equal to all values of a tree *) + predicate ge_tree (v:int) (t:tree) = + match t with + | Null -> true + | Tree x l r -> v >= x /\ ge_tree v l /\ ge_tree v r + end + + lemma ge_trans : forall t:tree, x y:int. + x >= y /\ ge_tree y t -> ge_tree x t + +end + +module TreeMax + + use import int.Int + use int.MinMax + use import BinTree + + let rec max_aux (t:tree) (acc:int) = + { true } + match t with + | Null -> acc + | Tree v l r -> + max_aux l (max_aux r (MinMax.max v acc)) + end + { ge_tree result t /\ result >= acc /\ + (result = acc \/ mem result t) } + + let max (t: tree) = + { t <> Null } + match t with + | Null -> absurd + | Tree v l r -> + max_aux l (max_aux r v) + end + { ge_tree result t /\ mem result t } + +end + +(* +Local Variables: +compile-command: "why3ide tree_max.mlw" +End: +*) + +