CodeTools[ProgramAnalysis]
|
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 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
|
|
>
|
|
|
Straight-Forward Invariant Calculation
|
|
|
Consider the following procedure that computes a factor for 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;
|
| (1) |
>
|
|
| (2) |
| (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 divided by :
|
>
|
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.
|
>
|
|
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 have constraints that are not yet being taken into consideration. The randomly generated parameters are both positive and negative values, ignoring the fact that and . 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:
|
>
|
|
| (4) |
>
|
|
•
|
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:
|
>
|
|
|
|
|
Compatibility
|
|
•
|
The CodeTools[ProgramAnalysis][LoopInvariant] command was introduced in Maple 2016.
|
|
|