Verify Loop - Maple Help

CodeTools[ProgramAnalysis]

 VerifyLoop
 verify if a WhileLoop satisfies its post-condition

 Calling Sequence VerifyLoop(loop, invariant, options)

Parameters

 loop - invariant - boolean function; invariant of loop options - (optional) sequence of equations, as listed in the Options section below

Options

 • 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.

Description

 • 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.

Examples

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

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;
 ${\mathrm{z3sqrt}}{≔}{\mathbf{proc}}\left({a}{,}{\mathrm{err}}\right)\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{local}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{r}{,}{q}{,}{p}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{r}{≔}{a}{-}{1}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{q}{≔}{1}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{p}{≔}{1}{/}{2}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathrm{ASSERT}}{}\left({a}{<=}{4}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{1}{<=}{a}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{0}{<}{\mathrm{err}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{0}{<}{p}\right){;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{while}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathrm{err}}{<=}{2}{*}{p}{*}{r}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{do}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{if}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{0}{<=}{2}{*}{r}{-}{2}{*}{q}{-}{p}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{then}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{r}{≔}{2}{*}{r}{-}{2}{*}{q}{-}{p}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{q}{≔}{q}{+}{p}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{p}{≔}{1}{/}{2}{*}{p}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{else}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{r}{≔}{2}{*}{r}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{p}{≔}{1}{/}{2}{*}{p}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{end if}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{end do}}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathrm{ASSERT}}{}\left({q}{^}{2}{<=}{a}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{a}{<}{q}{^}{2}{+}{\mathrm{err}}\right){;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{return}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{q}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{end proc}}$ (1)

Construct the WhileLoop data structure:

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

Compute the absolute invariants of loop:

 > $\mathrm{invariant}≔\mathrm{LoopInvariant}\left(\mathrm{loop},\mathrm{invarianttype}=\mathrm{absolute}\right)$
 ${\mathrm{invariant}}{≔}{2}{}{p}{}{r}{+}{{q}}^{{2}}{-}{a}{=}{0}$ (3)

The verification of the loop fails in this case because the pre-condition is not strong enough:

 > $\mathrm{verification_counter_examples}≔\mathrm{VerifyLoop}\left(\mathrm{loop},\mathrm{invariant},\mathrm{output}=\mathrm{counterexample}\right)$
 ${\mathrm{verification_counter_examples}}{≔}\left[{\mathrm{polynomial_ring}}{,}\left[{\mathrm{regular_semi_algebraic_system}}{,}{\mathrm{regular_semi_algebraic_system}}{,}{\mathrm{regular_semi_algebraic_system}}{,}{\mathrm{regular_semi_algebraic_system}}{,}{\mathrm{regular_semi_algebraic_system}}\right]\right]$ (4)

The RegularChains:-Display command can be used to see what values of the loop variables violate the post-conditions:

 > $\mathrm{RegularChains}:-\mathrm{Display}\left(\mathrm{verification_counter_examples}\left[2\right]\left[1\right],\mathrm{verification_counter_examples}\left[1\right]\right)$
 $\left\{\begin{array}{cc}{a}{-}{2}{}{r}{}{p}{-}{{q}}^{{2}}{=}{0}& {}\\ {2}{}{r}{}{p}{+}{{q}}^{{2}}{-}{4}{=}{0}& {}\\ {q}{<}{-2}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathrm{err}}{>}{0}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{r}{<}{0}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{{q}}^{{2}}{+}{\mathrm{err}}{-}{4}{\ne }{0}& {}\end{array}\right\$ (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:

 > $\mathrm{VerifyLoop}\left(\mathrm{loop},\mathrm{And}\left(\mathrm{invariant},0\le r\right)\right)$
 ${\mathrm{true}}$ (6)

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.

Compatibility

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