CodeTools[ProgramAnalysis] - Maple Programming Help

Home : Support : Online Help : Programming : CodeTools : Program Analysis : CodeTools/ProgramAnalysis/LoopInvariant

CodeTools[ProgramAnalysis]

 LoopInvariant
 compute an invariant of a WhileLoop

 Calling Sequence LoopInvariant(loop, knowninvariants, options) LoopInvariant(loop, knowninvariants, totaldegree = td, options) LoopInvariant(loop, knowninvariants, monomials = monoms, options)

Parameters

 loop - WhileLoop to analyze td - posint, the total degree of the monomials used in interpolating the loop's sample points monoms - list(polynom), the monomials to be used as a basis when computing the loop invariant knowninvariants - (optional) see IsLoopInvariant for the format of an invariant options - (optional) sequence of equations, as listed in the Options section below

Options

 • invarianttype = plain (default), inductive or absolute
 Specifies the type of invariant to compute, either a plain invariant, an inductive invariant or an absolute invariant
 • checkresults = true (default) or false
 Specifies whether or not the generated invariants are verified using IsLoopInvariant
 • numberofprimes = np, where np is a non-negative integer
 Specifies the number of primes used in the interpolation.  Default is np = 2.
 • numberofsamples = ns, where ns is a positive integer
 Specifies the number of samples to generate using TrajectoryPoints.  The default value is computed from the loop's properties.
 • parameterprocedure = pproc, where pproc is a procedure
 Specifies a procedure that computes values to be used for loop's parameters when generating trajectory sample points.  pproc accepts no arguments and returns a list with one value for each name in loop:-parameters.
 • parametervalues = pvs where pvs is a listlist
 Specifies values for the parameters when generating trajectory sample points.  Each sub-list has the same number of elements as there are names in loop:-parameters.

Description

 • This command computes a polynomial equational invariant of loop.  The method works by generating sample loop trajectories (using TrajectoryPoints).  Those sample points are then interpolated to find polynomial equations that may be an invariant of the loop.  Given a large enough number of primes np, number of sample points ns, number of good seed points (generated by the procedure in pproc or supplied through the list of points pvs), and basis for the interpolation (either a large td or a complete list of monoms up to a high degree), the command will likely generate a loop invariant.  If any of these elements is deficient, spurious equations will be included in the resulting system and it will not be an invariant of the loop.  By default, the result is checked using IsLoopInvariant to ensure that the generated equations are indeed a loop invariant, although this step can be skipped using the checkresults = false option.
 • The return value is an equation or a boolean function of equations.
 • The optional known invariants knowninvariants are used to filter out invalid parameter values when generating the loop trajectories as well as to validate the generated polynomial equations.  In some cases, the equations themselves are not invariants, but are invariants when combined with other relations.  See VerifyLoop for such an example.
 • The type of invariant computed is determined by the invarianttype option.  By default, plain invariants are computed, but invarianttype = inductive or invarianttype = absolute can be specified to generate inductive or absolute invariants.
 • The interpolation can be performed modulo some primes and the result reconstructed from the result.  Using primes slightly smaller than the machine precision integers give the fastest computations.  By default 2 primes are used, but additional primes may be used by specifying a larger np.  Alternatively, numberofprimes = 0 can be specified to conduct the calculations without modular arithmetic.
 • The basis for the interpolation are the monomials in the loop's variables and parameters.  By default, monomials up to degree three are used, but this can be increased by specifying td.  Alternatively, the list of monomials to be used can be given in monoms.
 • The number of samples used in the interpolation is controlled via the ns option.  The default number of samples used is inferred based on the number of variables in the loop and the total degree of the monomials.
 • The loop trajectories used for the interpolation points are generated using random values for the loop's parameters that provide the initial points in a series of loop trajectories.  These parameter values are input values for the loop that ideally make the loop iterate many times.  If the automatic process is incapable of generating sufficient sample points or there are special relationships between the parameters of the loop, sensible parameter values or a procedure that generates such values can be given.  A list of parameter values can be supplied via the parametervalues option.  Alternatively, a procedure to compute parameter values can be provided via the parameterprocedure option.  In all cases, the parameter values that are inconsistent with the loop's pre-conditions or the given known invariants are automatically discarded.

Examples

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

Straight-Forward Invariant Calculation

 Consider the following procedure that computes a factor for $N$ based on Fermat's factorization method:
 > divisor := proc (N, R)     local u, v, r;     u := 2 * R + 1;     v := 1;     r := R * R - N;     ASSERT(N >= 1 and (R-1)*(R-1) < N and N <= R*R);     while (r <> 0) do         if (r > 0) then             r := r - v;             v := v + 2;         else             r := r + u;             u := u + 2;         end if;     end do;     ASSERT(u <> v);     return ((u - v) / 2); end proc;
 ${\mathrm{divisor}}{≔}{\mathbf{proc}}\left({N}{,}{R}\right)\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{local}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{u}{,}{v}{,}{r}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{u}{≔}{2}{*}{R}{+}{1}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{v}{≔}{1}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{r}{≔}{R}{*}{R}{-}{N}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathrm{ASSERT}}{}\left({1}{<=}{N}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}\left({R}{-}{1}\right){*}\left({R}{-}{1}\right){<}{N}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{N}{<=}{R}{*}{R}\right){;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{while}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{r}{<>}{0}\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}{<}{r}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{then}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{r}{≔}{r}{-}{v}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{v}{≔}{v}{+}{2}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{else}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{r}{≔}{r}{+}{u}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{u}{≔}{u}{+}{2}\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({u}{<>}{v}\right){;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{return}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{1}{/}{2}{*}{u}{-}{1}{/}{2}{*}{v}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{end proc}}$ (1)
 Construct the WhileLoop data structure:
 > $\mathrm{loop}≔\mathrm{CreateLoop}\left(\mathrm{divisor}\right)$
 ${\mathrm{loop}}{≔}{\mathrm{Record}}{}\left({\mathrm{WhileLoop}}{,}{\mathrm{variables}}{=}\left[{r}{,}{u}{,}{v}\right]{,}{\mathrm{parameters}}{=}\left[{N}{,}{R}\right]{,}{\mathrm{initialization}}{=}\left[{{R}}^{{2}}{-}{N}{,}{2}{}{R}{+}{1}{,}{1}\right]{,}{\mathrm{transitions}}{=}\left[\left[{0}{<}{r}{,}\left[{r}{-}{v}{,}{u}{,}{v}{+}{2}\right]\right]{,}\left[\left[{}\right]{,}\left[{r}{+}{u}{,}{u}{+}{2}{,}{v}\right]\right]\right]{,}{\mathrm{guard}}{=}\left({r}{\ne }{0}\right){,}{\mathrm{precondition}}{=}\left[\left[\left[{1}{\le }{N}{,}{\left({R}{-}{1}\right)}^{{2}}{<}{N}\right]{,}{N}{\le }{{R}}^{{2}}\right]\right]{,}{\mathrm{postcondition}}{=}\left[{u}{\ne }{v}\right]{,}{\mathrm{returnvalue}}{=}\left[\frac{{1}}{{2}}{}{u}{-}\frac{{1}}{{2}}{}{v}\right]\right)$ (2)
 A loop invariant is:
 > $\mathrm{inv}≔\mathrm{LoopInvariant}\left(\mathrm{loop}\right)$
 Warning, found 14 initial points, but sought 15 points.  The default means of generating parameters values may not be able create sufficient initial points so that enough loop samples can be computed.  If the invariant cannot be verified, provide a list of valid input parameters for the loop or a procedure that can generate random valid parameters.
 ${\mathrm{inv}}{≔}{{u}}^{{2}}{-}{{v}}^{{2}}{-}{4}{}{N}{-}{4}{}{r}{-}{2}{}{u}{+}{2}{}{v}{=}{0}$ (3)
 which means that this equation will be satisfied before and after every iteration of loop.

Generating More Trajectory Points for Structured Problems

 The loop in the following procedure computes the floor of $\mathrm{x1}$ divided by $\mathrm{x2}$:
 > mannadivision := proc(x1 :: nonnegint, x2 :: posint)     local y1, y2, y3;     y1 := 0;     y2 := 0;     y3 := x1;     while (y3 <> 0) do         if (y2 + 1 = x2) then             y1 := y1 + 1;             y2 := 0;             y3 := y3 - 1;         else             y2 := y2 + 1;             y3 := y3 - 1;         end if;     end do;     return y1; end proc: loop :=  CreateLoop(mannadivision):
 In this case, the candidate invariant cannot be verified.  The computed invariant likely includes spurious polynomials.
 > $\mathrm{inv}≔\mathrm{LoopInvariant}\left(\mathrm{loop}\right):$
 The inputs for the procedure $\mathrm{mannadivision}$ have constraints that are not yet being taken into consideration.  The randomly generated parameters are both positive and negative values, ignoring the fact that $0\le \mathrm{x1}$ and $0<\mathrm{x2}$.  RandomTools:-Generate is used to generate a procedure that will encode these constraints when computing parameter values for the loop and LoopInvariant is called again:
 > $p≔\mathrm{RandomTools}:-\mathrm{Generate}\left(\left[\mathrm{integer}\left(\mathrm{range}=0..500\right),\mathrm{integer}\left(\mathrm{range}=1..10\right)\right],\mathrm{makeproc}\right)$
 ${p}{≔}{\mathbf{proc}}\left({}\right)\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathrm{eval}}{}\left(\left[{\mathrm{RandomTools:-Generate}}{}\left({\mathrm{integer}}{}\left({\mathrm{range}}{=}{0}{..}{500}\right)\right){,}{\mathrm{RandomTools:-Generate}}{}\left({\mathrm{integer}}{}\left({\mathrm{range}}{=}{1}{..}{10}\right)\right)\right]\right)\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{end proc}}$ (4)
 > $\mathrm{inv}≔\mathrm{LoopInvariant}\left(\mathrm{loop},\mathrm{parameterprocedure}=p\right):$
 • Spurious invariants are still being generated, which means that trying a larger number of sample points should help isolate the true invariant of the loop:
 > $\mathrm{inv}≔\mathrm{LoopInvariant}\left(\mathrm{loop},\mathrm{parameterprocedure}=p,\mathrm{numberofsamples}=400\right)$
 ${\mathrm{inv}}{≔}{\mathrm{x2}}{}{\mathrm{y1}}{-}{\mathrm{x1}}{+}{\mathrm{y2}}{+}{\mathrm{y3}}{=}{0}$ (5)

Compatibility

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