gallery: foveoos11_challenge1 using auto-deref

parent 5a289fd1
......@@ -11,20 +11,19 @@ module Max
use ref.Refint
use array.Array
let max (a: array int)
let max (a: array int) : 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
let y = ref (length a - 1) in
while !x <> !y do
invariant { 0 <= !x <= !y < length a }
invariant {
forall i: int. (0 <= i < !x \/ !y < i < length a) ->
(a[i] <= a[!y] \/ a[i] <= a[!x]) }
variant { !y - !x }
if a[!x] <= a[!y] then incr x else decr y
ensures { 0 <= result < length a }
ensures { forall i. 0 <= i < length a -> a[i] <= a[result] }
= let ref x = 0 in
let ref y = (length a - 1) in
while x <> y do
invariant { 0 <= x <= y < length a }
invariant { forall i. (0 <= i < x \/ y < i < length a) ->
(a[i] <= a[y] \/ a[i] <= a[x]) }
variant { y - x }
if a[x] <= a[y] then incr x else decr y
done;
!x
x
end
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment