mirror of
https://github.com/kmc7468/cs220.git
synced 2025-12-12 21:08:45 +00:00
30 lines
735 B
Plaintext
30 lines
735 B
Plaintext
(* Max
|
|
|
|
Given an array `a` of natural numbers with length `n`,
|
|
return the maximum element of the array.
|
|
|
|
You should stengthen the loop invariant.
|
|
*)
|
|
|
|
module Max
|
|
|
|
use int.Int
|
|
use ref.Ref
|
|
use array.Array
|
|
|
|
let max (a: array int) (n: int) : (max: int)
|
|
requires { n = length a }
|
|
requires { forall i. 0 <= i < n -> a[i] >= 0 }
|
|
ensures { forall i. 0 <= i < n -> a[i] <= max }
|
|
ensures { exists i. 0 <= i < n -> a[i] = max }
|
|
= let ref max = 0 in
|
|
for i = 0 to n - 1 do
|
|
(* IMPORTANT: DON'T MODIFY THE ABOVE LINES *)
|
|
invariant { true (* TODO: Replace `true` with your solution *) }
|
|
(* IMPORTANT: DON'T MODIFY THE BELOW LINES *)
|
|
if max < a[i] then max <- a[i];
|
|
done;
|
|
max
|
|
|
|
end
|