This command checks if candinv is an invariant of the WhileLoop loop, returning true if it is and false if it is not.

If any additional invariants of loop are known, they can be given using the optional argument knowninv.  The known invariants are used to create weaker candidate invariants from candinv by forming the conjunction of knowninv and candinv.

Boolean functions are used to represent candinv and knowninv.  If boolean operators were used, the relations will evaluate prematurely to true or false.  In the case of absolute invariants, only a single polynomial equation or an And of polynomial equations are supported.

The value of invtype determines what kind of invariant test is being conducted.  By default, it will be checked if candinv is a plain invariant of loop when invtype is plain.  It can also be verified if candinv is an inductive or absolute invariant when invtype is inductive or absolute.

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

Fibonacci := proc(n)
    local x, y, t;
    x := 0;
    y := 1;
    t := 0;
    while (y <= n) do
        t := y;
        y := x + y;
        x := t;
   end do:
   return x:
end proc;

$\mathrm{Fibonacci}≔\mathbf{proc}\left(n\right)\mathbf{local}x\&comma;y\&comma;t\&semi;x≔0\&semi;y≔1\&semi;t≔0\&semi;\mathbf{while}y<=n\mathbf{do}t≔y\&semi;y≔x\&plus;y\&semi;x≔t\mathbf{end\; do}\&semi;\mathbf{return}x\mathbf{end\; proc}$

$\mathrm{loop}≔\mathrm{CreateLoop}\left(\mathrm{Fibonacci}\right)$

$\mathrm{loop}≔\mathrm{Record}\left(\mathrm{WhileLoop}\&comma;\mathrm{variables}=\left[t\&comma;x\&comma;y\right]\&comma;\mathrm{parameters}=\left[n\right]\&comma;\mathrm{initialization}=\left[0\&comma;0\&comma;1\right]\&comma;\mathrm{transitions}=\left[\left[\left[\right]\&comma;\left[y\&comma;y\&comma;x+y\right]\right]\right]\&comma;\mathrm{guard}=\left(y\le n\right)\&comma;\mathrm{precondition}=\left[\right]\&comma;\mathrm{postcondition}=\left[\right]\&comma;\mathrm{returnvalue}=\left[x\right]\right)$

$\mathrm{IsLoopInvariant}\left(\mathrm{loop}\&comma;\left[1+x^2{y}^2-2x^{3}y+2y^{3}x-y^4-x^4=0\right]\&comma;\mathrm{invarianttype}=\mathrm{absolute}\right)$

$\mathrm{true}$

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

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