CodeTools[ProgramAnalysis] - Maple Programming Help

Online Help

All Products    Maple    MapleSim


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

CodeTools[ProgramAnalysis]

  

LoopInvariant

  

compute an invariant of a WhileLoop

 

Calling Sequence

Parameters

Options

Description

Examples

Compatibility

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

withCodeTools[ProgramAnalysis]:

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;

divisorprocN&comma;Rlocalu&comma;v&comma;r&semi;u2&ast;R&plus;1&semi;v1&semi;rR&ast;RN&semi;ASSERT1<=NandR1&ast;R1<NandN<=R&ast;R&semi;whiler<>0doif0<rthenrrv&semi;vv&plus;2elserr&plus;u&semi;uu&plus;2end ifend do&semi;ASSERTu<>v&semi;return1&sol;2&ast;u1&sol;2&ast;vend proc

(1)
  

Construct the WhileLoop data structure:

loopCreateLoopdivisor

loopRecordWhileLoop&comma;variables&equals;r&comma;u&comma;v&comma;parameters&equals;N&comma;R&comma;initialization&equals;R2N&comma;2R&plus;1&comma;1&comma;transitions&equals;0<r&comma;rv&comma;u&comma;v&plus;2&comma;&comma;r&plus;u&comma;u&plus;2&comma;v&comma;guard&equals;r0&comma;precondition&equals;1N&comma;R12<N&comma;NR2&comma;postcondition&equals;uv&comma;returnvalue&equals;12u12v

(2)
  

A loop invariant is:

invLoopInvariantloop

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.  

invu2v24N4r2u&plus;2v&equals;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 x1 divided by 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.

invLoopInvariantloop&colon;

Error, (in CodeTools:-ProgramAnalysis:-LoopInvariant) the computed candidate invariant cannot be verified: [x2*y1-x1+y2+y3 = 0, x1^2-x1*x2-7*x1*y1-2*x1*y2-2*x1*y3+x2*y2+x2*y3+6*y1^2+7*y1*y2+7*y1*y3+y2^2+2*y2*y3+y3^2+7*x1-6*y1-7*y2-7*y3 = 0, -61*x1^2*x2-169*x1*x2^2+61*x1*x2*y2+61*x1*x2*y3+169*x2^2*y2+169*x2^2*y3+1204*x1^2+4091*x1*x2-5343*x1*y1-1204*x1*y2-1204*x1*y3-4091*x2*y2-4091*x2*y3-29497*x1+63375*y1+29497*y2+29497*y3 = 0, -61*x1^2*x2-399*x1*x2^2+399*x2^2*y2+399*x2^2*y3+61*x2*y2^2+122*x2*y2*y3+61*x2*y3^2+1981*x1^2+8609*x1*x2-10320*x1*y1-1554*x1*y2-1554*x1*y3-8609*x2*y2-8609*x2*y3-366*y1*y2-366*y1*y3-427*y2^2-854*y2*y3-427*y3^2-59360*x1+126750*y1+59360*y2+59360*y3 = 0, -610*x1^3+610*x1^2*y2+610*x1^2*y3+1993*x1*x2^2-1993*x2^2*y2-1993*x2^2*y3-20325*x1^2-55934*x1*x2+73905*x1*y1+20325*x1*y2+20325*x1*y3+55934*x2*y2+55934*x2*y3+365212*x1-744081*y1-365212*y2-365212*y3 = 0, 610*x1^2*y1+159*x1*x2^2-159*x2^2*y2-159*x2^2*y3+925*x1^2-4242*x1*x2+2615*x1*y1-925*x1*y2-925*x1*y3+4242*x2*y2+4242*x2*y3+43926*x1-121113*y1-43926*y2-43926*y3 = 0, -610*x1^2*y3-28517*x1*x2^2-8540*x1*x2*y3+610*x1*y2*y3+610*x1*y3^2+28517*x2^2*y2+28517*x2^2*y3+8540*x2*y2*y3+8540*x2*y3^2+84101*x1^2+527990*x1*x2-582621*x1*y1-150957*x1*y2-32007*x1*y3-527990*x2*y2-527990*x2*y3+401136*y1*y2-38064*y1*y3+66856*y2^2+14762*y2*y3-52094*y3^2-3507462*x1+7494669*y1+3507462*y2+3507462*y3 = 0, 11977*x1*x2^2+3050*x1*x2*y3+1830*x1*y1*y3-11977*x2^2*y2-11977*x2^2*y3-3050*x2*y2*y3-3050*x2*y3^2-40833*x1^2-232038*x1*x2+279753*x1*y1+70601*x1*y2+26071*x1*y3+232038*x2*y2+232038*x2*y3-178608*y1*y2-4758*y1*y3-29768*y2^2-15006*y2*y3+14762*y3^2+1601870*x1-3532089*y1-1601870*y2-1601870*y3 = 0, -305*x1^3+610*x1^2*y3+31355*x1*x2^2+8540*x1*x2*y3+305*x1*y2^2-305*x1*y3^2-31355*x2^2*y2-31355*x2^2*y3-8540*x2*y2*y3-8540*x2*y3^2-106603*x1^2-608222*x1*x2+676653*x1*y1+169616*x1*y2+50666*x1*y3+608222*x2*y2+608222*x2*y3-394548*y1*y2+44652*y1*y3-63013*y2^2-7076*y2*y3+55937*y3^2+4026747*x1-8555625*y1-4026747*y2-4026747*y3 = 0, -1150*x1*x2^2-305*x1*x2*y3+183*x1*y1*y2+1150*x2^2*y2+1150*x2^2*y3+305*x2*y2*y3+305*x2*y3^2+3885*x1^2+22590*x1*x2-24885*x1*y1-6203*x1*y2-1750*x1*y3-22590*x2*y2-22590*x2*y3+15555*y1*y2-1830*y1*y3+2318*y2^2+183*y2*y3-2135*y3^2-149315*x1+316875*y1+149315*y2+149315*y3 = 0, -3050*x1^3-610*x1^2*y3+25215*x1*x2^2-11590*x1*x2*y3-25215*x2^2*y2-25215*x2^2*y3+11590*x2*y2*y3+11590*x2*y3^2+3660*y1*y2*y3+3660*y1*y3^2+3050*y2^3+9760*y2^2*y3+10370*y2*y3^2+3660*y3^3-223869*x1^2-1035826*x1*x2+1077369*x1*y1-25377*x1*y2+127123*x1*y3+1035826*x2*y2+1035826*x2*y3+671976*y1*y2+141276*y1*y3+249246*y2^2+345992*y2*y3+96746*y3^2+6318466*x1-12742305*y1-6318466*y2-6318466*y3 = 0, 610*x1^2*y3+33875*x1*x2^2+11590*x1*x2*y3-33875*x2^2*y2-33875*x2^2*y3-11590*x2*y2*y3-11590*x2*y3^2+3050*y1*y2^2+2440*y1*y2*y3-610*y1*y3^2-610*y2^2*y3-1220*y2*y3^2-610*y3^3-102651*x1^2-589324*x1*x2+670051*x1*y1+203667*x1*y2+51167*x1*y3+589324*x2*y2+589324*x2*y3-496296*y1*y2+34404*y1*y3-101016*y2^2-49532*y2*y3+51484*y3^2+3979574*x1-8530725*y1-3979574*y2-3979574*y3 = 0, -61*x1*x2^3+61*x2^3*y2+61*x2^3*y3+1846*x1*x2^2-1846*x2^2*y2-1846*x2^2*y3-210*x1^2-19193*x1*x2+2730*x1*y1+210*x1*y2+210*x1*y3+19193*x2*y2+19193*x2*y3+77954*x1-83226*y1-77954*y2-77954*y3 = 0, -x1*x2^2*y3+x2^2*y2*y3+x2^2*y3^2-15*x1*x2^2+23*x1*x2*y3+15*x2^2*y2+15*x2^2*y3-23*x2*y2*y3-23*x2*y3^2-21*x1^2+366*x1*x2+21*x1*y1+77*x1*y2-97*x1*y3-366*x2*y2-366*x2*y3-336*y1*y2+96*y1*y3-56*y2^2+62*y2*y3+118*y3^2-2106*x1+1755*y1+2106*y2+2106*y3 = 0]

  

The inputs for the procedure 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 0x1 and 0<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:

pRandomTools:-Generateintegerrange&equals;0..500&comma;integerrange&equals;1..10&comma;makeproc

pprocevalRandomTools:-Generateintegerrange&equals;0..500&comma;RandomTools:-Generateintegerrange&equals;1..10end proc

(4)

invLoopInvariantloop&comma;parameterprocedure&equals;p&colon;

Error, (in CodeTools:-ProgramAnalysis:-LoopInvariant) the computed candidate invariant cannot be verified: [x2*y1-x1+y2+y3 = 0, -x1^3+3*x1^2*x2+3*x1^2*y1+3*x1^2*y2+3*x1^2*y3-2*x1*x2^2-6*x1*x2*y2-6*x1*x2*y3-2*x1*y1^2-6*x1*y1*y2-6*x1*y1*y3-3*x1*y2^2-6*x1*y2*y3-3*x1*y3^2+2*x2^2*y2+2*x2^2*y3+3*x2*y2^2+6*x2*y2*y3+3*x2*y3^2+2*y1^2*y2+2*y1^2*y3+3*y1*y2^2+6*y1*y2*y3+3*y1*y3^2+y2^3+3*y2^2*y3+3*y2*y3^2+y3^3-9*x1^2+6*x1*x2+6*x1*y1+18*x1*y2+18*x1*y3-6*x2*y2-6*x2*y3-6*y1*y2-6*y1*y3-9*y2^2-18*y2*y3-9*y3^2-4*x1+4*y2+4*y3 = 0, 3*x1^3-9*x1^2*x2-7*x1^2*y1-9*x1^2*y2-9*x1^2*y3+6*x1*x2^2+18*x1*x2*y2+18*x1*x2*y3+14*x1*y1*y2+14*x1*y1*y3+9*x1*y2^2+18*x1*y2*y3+9*x1*y3^2-6*x2^2*y2-6*x2^2*y3-9*x2*y2^2-18*x2*y2*y3-9*x2*y3^2+4*y1^3-7*y1*y2^2-14*y1*y2*y3-7*y1*y3^2-3*y2^3-9*y2^2*y3-9*y2*y3^2-3*y3^3+21*x1^2-14*x1*x2-42*x1*y2-42*x1*y3+14*x2*y2+14*x2*y3-12*y1^2+21*y2^2+42*y2*y3+21*y3^2+8*y1 = 0, -x1^3*x2+3*x1^2*x2^2+3*x1^2*x2*y2+3*x1^2*x2*y3-2*x1*x2^3-6*x1*x2^2*y2-6*x1*x2^2*y3-3*x1*x2*y2^2-6*x1*x2*y2*y3-3*x1*x2*y3^2+2*x2^3*y2+2*x2^3*y3+3*x2^2*y2^2+6*x2^2*y2*y3+3*x2^2*y3^2+x2*y2^3+3*x2*y2^2*y3+3*x2*y2*y3^2+x2*y3^3+3*x1^3-9*x1^2*x2-2*x1^2*y1-9*x1^2*y2-9*x1^2*y3+6*x1*x2^2+18*x1*x2*y2+18*x1*x2*y3+4*x1*y1*y2+4*x1*y1*y3+9*x1*y2^2+18*x1*y2*y3+9*x1*y3^2-6*x2^2*y2-6*x2^2*y3-9*x2*y2^2-18*x2*y2*y3-9*x2*y3^2-2*y1*y2^2-4*y1*y2*y3-2*y1*y3^2-3*y2^3-9*y2^2*y3-9*y2*y3^2-3*y3^3+6*x1^2-4*x1*x2-12*x1*y2-12*x1*y3+4*x2*y2+4*x2*y3+6*y2^2+12*y2*y3+6*y3^2 = 0]

• 

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:

invLoopInvariantloop&comma;parameterprocedure&equals;p&comma;numberofsamples&equals;400

invx2y1x1&plus;y2&plus;y3&equals;0

(5)

Compatibility

• 

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

• 

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