Commit 3f02264b authored by MARCHE Claude's avatar MARCHE Claude

FoVeOOS competition

parent 275353b3
(*
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:
*)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment