verify if a WhileLoop satisfies its post-condition
VerifyLoop(loop, invariant, options)
boolean function; invariant of loop
(optional) sequence of equations, as listed in the Options section below
checkinvariants = false (default) or true
Specifies whether or not the invariant invariant should be checked using IsLoopInvariant
invarianttype = plain, inductive or absolute
Specifies the type of invariant check to be performed on invariant, either a plain invariant, an inductive invariant or an absolute invariant
output = truefalse (default) or counterexample, or a list thereof
Specify the command's output. By default, the command returns a truefalse value stating whether or not the post-condition holds. When counterexample is given, a list with the polynomial ring RegularChains[PolynomialRing] of the system and a sub-list of regular semi-algebraic systems that violate the post-condition is returned (see the SemiAlgebraicSetTools package for details on working with regular semi-algebraic systems). The counter example will be the empty set (represented by an empty list) when loop is guaranteed to satisfy its post-condition.
This command verifies whether or not loop's post-condition is true given its pre-condition, the negation of its guard condition and the loop invariant inv. The pre-, post- and guard conditions were all extracted from the ASSERT statements in the original procedure when CreateLoop was called.
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:
r := 2 * r;
p := 1/2 * p:
ASSERT(q^2 <= a and a < q^2+err);
z3sqrt ≔ proca,errlocalr,q,p;r ≔ a − 1;q ≔ 1;p ≔ 1/2;ASSERT⁡a<=4and1<=aand0<errand0<p;whileerr<=2*p*rdoif0<=2*r − 2*q − pthenr ≔ 2*r − 2*q − p;q ≔ q+p;p ≔ 1/2*pelser ≔ 2*r;p ≔ 1/2*pend ifend do;ASSERT⁡q^2<=aanda<q^2+err;returnqend proc
Construct the WhileLoop data structure:
loop ≔ CreateLoop⁡z3sqrt
Compute the absolute invariants of loop:
invariant ≔ LoopInvariant⁡loop,invarianttype=absolute
The verification of the loop fails in this case because the pre-condition is not strong enough:
verification_counter_examples ≔ VerifyLoop⁡loop,invariant,output=counterexample
The RegularChains:-Display command can be used to see what values of the loop variables violate the post-conditions:
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.
The CodeTools[ProgramAnalysis][VerifyLoop] command was introduced in Maple 2016.
For more information on Maple 2016 changes, see Updates in Maple 2016.
Download Help Document