## 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 import int.Int use import ref.Refint use import array.Array let max (a: array int) requires { length a > 0 } ensures { 0 <= result < length a } ensures { forall i: int. 0 <= i < length a -> a[i] <= a[result] } = let x = ref 0 in let y = ref (length a - 1) in while !x <> !y do invariant { 0 <= !x <= !y < length a } invariant { forall i: int. (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