Wiki Agenda Contact English version

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