examples/foveoos11_challenge1.mlw

   1
   2 (* FoVeOOS 2011 verification competition
   3    http://foveoos2011.cost-ic0701.org/verification-competition
   4
   5    Challenge 1
   6 *)
   7
   8 module Max
   9
  10   use int.Int
  11   use ref.Refint
  12   use array.Array
  13
  14   let max (a: array int) : int
  15     requires { length a > 0 }
  16     ensures  { 0 <= result < length a }
  17     ensures  { forall i. 0 <= i < length a -> a[i] <= a[result] }
  18   = let ref x = 0 in
  19     let ref y = (length a - 1) in
  20     while x <> y do
  21       invariant { 0 <= x <= y < length a }
  22       invariant { forall i. (0 <= i < x \/ y < i < length a) ->
  23                             (a[i] <= a[y] \/ a[i] <= a[x]) }
  24       variant   { y - x }
  25       if a[x] <= a[y] then incr x else decr y
  26     done;
  27     x
  28
  29 end