Wiki Agenda Contact Version française

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