>
|
|
The following procedure computes the square root of a positive number to within the given tolerance err. The ASSERT statements contain the pre- and post-conditions of the loop, which is considered to be the specification of the loop.
>
|
z3sqrt := proc (a, err)
local r, q, p;
r := a - 1;
q := 1;
p := 1/2;
ASSERT(a <= 4 and 1 <= a and 0 < err and p > 0);
while err <= 2 * p * r do
if 0 <= 2 * r - 2 * q - p then
r := 2 * r - 2 * q - p;
q := q + p;
p := 1/2 * p:
else
r := 2 * r;
p := 1/2 * p:
end if:
end do;
ASSERT(q^2 <= a and a < q^2+err);
return q:
end proc;
|
| (1) |
Construct the WhileLoop data structure:
| (2) |
Compute the absolute invariants of loop:
>
|
|
| (3) |
The verification of the loop fails in this case because the pre-condition is not strong enough:
>
|
|
| (4) |
The RegularChains:-Display command can be used to see what values of the loop variables violate the post-conditions:
>
|
|
| (5) |
The pre-condition did not include that r is always positive. Supplying this piece of information in addition to the computed invariant allows us to verify that post-condition is satisfied:
>
|
|
This means that the condition in the ASSERT statement at the end of z3sqrt will indeed always return true and that the square root will be within the desired accuracy.