Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

array_max.mlw 959 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46
(*
COST Verification Competition. vladimir@cost-ic0701.org

Challenge 1: Maximum in an array


Given: A non-empty integer array a.

Verify that the index returned by the method max() given below points to
an element maximal in the array.
*)


module ArrayMax

  use import int.Int
  use import int.MinMax
  use import module ref.Ref
  use import module array.Array

  let max (a: array int) =
    { 0 < length a }
    let x = ref 0 in
    let y = ref (length a - 1) in
    while !x <> !y do
      invariant { 0 <= !x <= !y < length a /\
                    forall i:int.
                    0 <= i < !x \/ !y < i < length a ->
                       a[i] <= max a[!x] a[!y]
                }
      variant { !y - !x }
      if a[!x] <= a[!y] then x := !x+1 else y := !y-1
    done;
    !x
    { 0 <= result < length a /\
      forall i:int. 0 <= i < a.length -> a[i] <= a[result] }

end

(*
Local Variables:
compile-command: "why3ide array_max.mlw"
End:
*)