## Find the maximal element in an array

Challenge 1 at FoVeOOs 2011 competition

**Authors:** Jean-Christophe Filliâtre

**Topics:** Array Data Structure

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