Is Loop Invariant - Maple Help

CodeTools[ProgramAnalysis]

 IsLoopInvariant
 verify if a condition is an invariant of a loop

 Calling Sequence IsLoopInvariant(loop, candinv, knowninv, invarianttype = invtype)

Parameters

 loop - candinv - boolean function of polynomial relations; candidate invariant to verify knowninv - (optional) boolean function in polynomial relations; known invariant of loop invtype - (optional) one of either plain (default), inductive or absolute ; type of invariant check to perform

Description

 • 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.

Examples

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

The following procedure computes the ${n}^{\mathrm{th}}$ Fibonacci number:

 > 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)\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{local}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{x}{,}{y}{,}{t}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{x}{≔}{0}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{y}{≔}{1}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{t}{≔}{0}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{while}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{y}{<=}{n}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{do}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{t}{≔}{y}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{y}{≔}{x}{+}{y}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{x}{≔}{t}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{end do}}{;}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{return}}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{x}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}{\mathbf{end proc}}$ (1)

Construct the WhileLoop data structure:

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

Check whether or not $-{x}^{4}-2{x}^{3}y+{x}^{2}{y}^{2}+2{y}^{3}x-{y}^{4}+1=0$ is an absolute invariant of loop:

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

Compatibility

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