foveoos11_challenge1.mlw 706 Bytes
Newer Older
1 2 3 4 5 6 7 8 9

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

   Challenge 1
*)

module Max

10 11 12
  use int.Int
  use ref.Refint
  use array.Array
13

14 15 16 17 18
  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
19 20
    let y = ref (length a - 1) in
    while !x <> !y do
21
      invariant { 0 <= !x <= !y < length a }
22 23
      invariant {
        forall i: int. (0 <= i < !x \/ !y < i < length a) ->
24
                       (a[i] <= a[!y] \/ a[i] <= a[!x]) }
25 26 27 28 29 30
      variant { !y - !x }
      if a[!x] <= a[!y] then incr x else decr y
    done;
    !x

end