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.

$\mathrm{with}\left(\mathrm{CodeTools}\left[\mathrm{ProgramAnalysis}\right]\right)\:$

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;

$\mathrm{z3sqrt}≔\mathbf{proc}\left(a\&comma;\mathrm{err}\right)\mathbf{local}r\&comma;q\&comma;p\&semi;r≔a-1\&semi;q≔1\&semi;p≔1\&sol;2\&semi;\mathrm{ASSERT}\left(a<=4\mathbf{and}1<=a\mathbf{and}0<\mathrm{err}\mathbf{and}0<p\right)\&semi;\mathbf{while}\mathrm{err}<=2\&ast;p\&ast;r\mathbf{do}\mathbf{if}0<=2\&ast;r-2\&ast;q-p\mathbf{then}r≔2\&ast;r-2\&ast;q-p\&semi;q≔q\&plus;p\&semi;p≔1\&sol;2\&ast;p\mathbf{else}r≔2\&ast;r\&semi;p≔1\&sol;2\&ast;p\mathbf{end\; if}\mathbf{end\; do}\&semi;\mathrm{ASSERT}\left(q\&Hat;2<=a\mathbf{and}a<q\&Hat;2\&plus;\mathrm{err}\right)\&semi;\mathbf{return}q\mathbf{end\; proc}$

$\mathrm{loop}≔\mathrm{CreateLoop}\left(\mathrm{z3sqrt}\right)$

$\mathrm{loop}≔\mathrm{Record}\left(\mathrm{WhileLoop}\&comma;\mathrm{variables}=\left[p\&comma;q\&comma;r\right]\&comma;\mathrm{parameters}=\left[a\&comma;\mathrm{err}\right]\&comma;\mathrm{initialization}=\left[\frac{1}{2}\&comma;1\&comma;a-1\right]\&comma;\mathrm{transitions}=\left[\left[0\le 2r-2q-p\&comma;\left[\frac{p}{2}\&comma;q+p\&comma;2r-2q-p\right]\right]\&comma;\left[\left[\right]\&comma;\left[\frac{p}{2}\&comma;q\&comma;2r\right]\right]\right]\&comma;\mathrm{guard}=\left(\mathrm{err}\le 2pr\right)\&comma;\mathrm{precondition}=\left[\left[\left[\left[a\le 4\&comma;1\le a\right]\&comma;0<\mathrm{err}\right]\&comma;0<p\right]\right]\&comma;\mathrm{postcondition}=\left[\left[q^2\le a\&comma;a<q^2+\mathrm{err}\right]\right]\&comma;\mathrm{returnvalue}=\left[q\right]\right)$

$\mathrm{invariant}≔\mathrm{LoopInvariant}\left(\mathrm{loop}\&comma;\mathrm{invarianttype}=\mathrm{absolute}\right)$

$\mathrm{invariant}≔2pr+q^2-a=0$

$\mathrm{verification\_counter\_examples}≔\mathrm{VerifyLoop}\left(\mathrm{loop}\&comma;\mathrm{invariant}\&comma;\mathrm{output}=\mathrm{counterexample}\right)$

$\mathrm{verification\_counter\_examples}≔\left[\mathrm{polynomial\_ring}\&comma;\left[\mathrm{regular\_semi\_algebraic\_system}\&comma;\mathrm{regular\_semi\_algebraic\_system}\&comma;\mathrm{regular\_semi\_algebraic\_system}\&comma;\mathrm{regular\_semi\_algebraic\_system}\&comma;\mathrm{regular\_semi\_algebraic\_system}\right]\right]$

$\mathrm{RegularChains}:-\mathrm{Display}\left(\mathrm{verification\_counter\_examples}\left[2\right]\left[1\right]\&comma;\mathrm{verification\_counter\_examples}\left[1\right]\right)$

$\left\{\begin{array}{cc}a-2rp-q^2=0& \\ 2rp+q^2-4=0& \\ q<\mathrm{-2}\mathbf{and}\mathrm{err}>0\mathbf{and}r<0\mathbf{and}{q}^2+\mathrm{err}-4\ne 0& \end{array}\right.$

$\mathrm{VerifyLoop}\left(\mathrm{loop}\&comma;\mathrm{And}\left(\mathrm{invariant}\&comma;0\le r\right)\right)$

$\mathrm{true}$

The CodeTools[ProgramAnalysis][VerifyLoop] command was introduced in Maple 2016.

For more information on Maple 2016 changes, see Updates in Maple 2016.