FoVeOOS competition

examples/foveoos2011/array_max.mlw

+(*
+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:
+*)
+
+