CodeTools[ProgramAnalysis]
LoopInvariant
compute an invariant of a WhileLoop
Calling Sequence
Parameters
Options
Description
Examples
Compatibility
LoopInvariant(loop, knowninvariants, options)
LoopInvariant(loop, knowninvariants, totaldegree = td, options)
LoopInvariant(loop, knowninvariants, monomials = monoms, options)
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
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.
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.
withCodeToolsProgramAnalysis:
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;
divisor ≔ procN,Rlocalu,v,r;u ≔ 2*R+1;v ≔ 1;r ≔ R*R − N;ASSERT1<=NandR − 1*R − 1<NandN<=R*R;whiler<>0doif0<rthenr ≔ r − v;v ≔ v+2elser ≔ u+r;u ≔ u+2end ifend do;ASSERTu<>v;return1/2*u − 1/2*vend proc
Construct the WhileLoop data structure:
loop≔CreateLoopdivisor
loop≔RecordWhileLoop,variables=r,u,v,parameters=N,R,initialization=R2−N,2R+1,1,transitions=0<r,r−v,u,v+2,,u+r,u+2,v,guard=r≠0,precondition=1≤N,R−12<N,N≤R2,postcondition=u≠v,returnvalue=u2−v2
A loop invariant is:
inv≔LoopInvariantloop
inv≔u2−v2−4N−4r−2u+2v=0
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.
inv≔LoopInvariantloop:
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 0≤x1 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:
p≔RandomTools:-Generateintegerrange=0..500,integerrange=1..10,makeproc
p ≔ procevalRandomTools:-Generateintegerrange=0..500,RandomTools:-Generateintegerrange=1..10end proc
inv≔LoopInvariantloop,parameterprocedure=p:
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:
inv≔LoopInvariantloop,parameterprocedure=p,numberofsamples=400
inv≔x2y1−x1+y2+y3=0
The CodeTools[ProgramAnalysis][LoopInvariant] command was introduced in Maple 2016.
For more information on Maple 2016 changes, see Updates in Maple 2016.
Download Help Document
