From 0b83243e56f8b60a4e79f00e236a30186dd3044d Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Thu, 6 Oct 2011 08:19:21 +0200 Subject: [PATCH] FoVeOOS competition --- examples/foveoos2011/array_max.mlw | 46 ++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 examples/foveoos2011/array_max.mlw diff --git a/examples/foveoos2011/array_max.mlw b/examples/foveoos2011/array_max.mlw new file mode 100644 index 000000000..e61f5dd60 --- /dev/null +++ b/examples/foveoos2011/array_max.mlw @@ -0,0 +1,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: +*) + + -- GitLab