Find the maximal element in an array
Challenge 1 at FoVeOOs 2011 competition
Auteurs: Jean-Christophe Filliâtre
Catégories: Array Data Structure
Outils: Why3
Références: 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 1 *) module Max use int.Int use ref.Refint use array.Array let max (a: array int) : int requires { length a > 0 } ensures { 0 <= result < length a } ensures { forall i. 0 <= i < length a -> a[i] <= a[result] } = let ref x = 0 in let ref y = (length a - 1) in while x <> y do invariant { 0 <= x <= y < length a } invariant { forall i. (0 <= i < x \/ y < i < length a) -> (a[i] <= a[y] \/ a[i] <= a[x]) } variant { y - x } if a[x] <= a[y] then incr x else decr y done; x end
download ZIP archive