Contact English version

L'équipe ProVal s'est arrêtée à la fin août 2012, et renaît en une nouvelle équipe Toccata
Ces pages n'évoluent plus, suivez le lien ci-dessus pour les informations à jour sur notre équipe.

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

index 


(* FoVeOOS 2011 verification competition
   http://foveoos2011.cost-ic0701.org/verification-competition

   Challenge 1
*)

module Max

  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