1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
(* Computing the square root (up to eps) using binary search
Note: precondition 0. < eps is not necessary for soundness
but needed to ensure termination.
*)
module BinarySqrt
use real.Real
use int.Int as Int
use real.MinMax as MinMax
use real.FromInt as FromInt
use real.Truncate as Truncate
let rec sqrt (r: real) (eps: real) (ghost n:int) (ghost eps0:real) : real
requires { 0.0 <= r }
requires { eps0 > 0.0 /\ Int.(>=) n 1 }
requires { eps = (FromInt.from_int n) * eps0 }
variant { Int.(-) (Truncate.ceil (MinMax.max r 1.0 / eps0)) n }
ensures { result * result <= r < (result + eps) * (result + eps) }
= if r < eps && 1.0 < eps then
0.0
else
begin
assert { FromInt.from_int n * eps0 <= MinMax.max r 1.0 };
assert { 1.0 / eps0 > 0.0 };
assert { FromInt.from_int n * eps0 * (1.0 / eps0) <= MinMax.max r 1.0 * (1.0 / eps0)};
assert { FromInt.from_int n * eps0 / eps0 <= MinMax.max r 1.0 / eps0};
assert { FromInt.from_int n <= MinMax.max r 1.0 / eps0 };
let r' = sqrt r (2.0 * eps) (Int.(*) 2 n) eps0 in
if (r' + eps) * (r' + eps) <= r then r' + eps else r'
end
let sqrt_main (r:real) (eps:real) : real
requires { 0.0 <= r }
requires { eps > 0.0 }
ensures { result * result <= r < (result + eps) * (result + eps) }
= sqrt r eps 1 eps
end
|
