mirror of
https://github.com/kmc7468/cs220.git
synced 2025-12-12 21:08:45 +00:00
38 lines
1.1 KiB
Plaintext
38 lines
1.1 KiB
Plaintext
(* Binary search
|
|
|
|
A classical example. Searches a sorted array for a given value v.
|
|
Consult <https://gitlab.inria.fr/why3/why3/-/blob/master/examples/binary_search.mlw>.
|
|
*)
|
|
|
|
module BinarySearch
|
|
|
|
use int.Int
|
|
use int.ComputerDivision
|
|
use ref.Ref
|
|
use array.Array
|
|
|
|
let binary_search (a : array int) (v : int) : int
|
|
requires { forall i1 i2 : int. 0 <= i1 < i2 < length a -> a[i1] <= a[i2] }
|
|
ensures { 0 <= result <= length a }
|
|
ensures { forall i: int. 0 <= i < result -> a[i] < v }
|
|
ensures { forall i: int. result <= i < length a -> v <= a[i] }
|
|
=
|
|
(* IMPORTANT: DON'T MODIFY THE ABOVE LINES *)
|
|
let ref l = 0 in
|
|
let ref r = length a in
|
|
while l < r do
|
|
invariant { 0 <= l <= length a /\ 0 <= r <= length a }
|
|
invariant { forall i: int. 0 <= i < l -> a[i] < v }
|
|
invariant { forall i: int. r <= i < length a -> a[i] >= v }
|
|
variant { r - l }
|
|
let m = l + div (r - l) 2 in
|
|
assert { l <= m < r };
|
|
if a[m] < v then
|
|
l := m + 1
|
|
else
|
|
r := m
|
|
done;
|
|
l
|
|
|
|
end
|