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
42
|
(********************************************************************
A simple algorithm for computing the square root of a non-negative
integer.
See file [sqrt_why.v] for the proofs of obligations generated by Why.
(c) Claude March 2002
**********************************************************************)
let sqrt = fun (x : int) ->
{ x >= 0 }
begin
if x = 0 then 0 else
if x <= 3 then 1 else
let y = ref x in
let z = ref (x+1)/2 in
begin
while !z < !y do
{ invariant
z > 0
and y > 0
and z = (x/y+y)/2
and x < (y+1)*(y+1)
and x < (z+1)*(z+1)
variant y}
y := !z;
z := (x / !z + !z) / 2
done;
!y
end
end
{ result * result <= x and x < (result+1)*(result+1) }
(*
Local Variables:
mode: tuareg
compile-command: "why sqrt.mlw"
End:
*)
|
