CodeTools[ProgramAnalysis] - Maple Programming Help

Online Help

All Products    Maple    MapleSim


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

CodeTools[ProgramAnalysis]

  

IsLoopInvariant

  

verify if a condition is an invariant of a loop

 

Calling Sequence

Parameters

Description

Examples

Compatibility

Calling Sequence

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

Parameters

loop

-

WhileLoop

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

withCodeTools[ProgramAnalysis]:

The following procedure computes the nth 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;

Fibonacciprocnlocalx&comma;y&comma;t&semi;x0&semi;y1&semi;t0&semi;whiley<=ndoty&semi;yx&plus;y&semi;xtend do&semi;returnxend proc

(1)

Construct the WhileLoop data structure:

loopCreateLoopFibonacci

loopRecordWhileLoop&comma;variables&equals;t&comma;x&comma;y&comma;parameters&equals;n&comma;initialization&equals;0&comma;0&comma;1&comma;transitions&equals;&comma;y&comma;y&comma;x&plus;y&comma;guard&equals;yn&comma;precondition&equals;&comma;postcondition&equals;&comma;returnvalue&equals;x

(2)

Check whether or not x42x3y&plus;x2y2&plus;2xy3y4&plus;1&equals;0 is an absolute invariant of loop:

IsLoopInvariantloop&comma;1&plus;x2y22x3y&plus;2y3xy4x4&equals;0&comma;invarianttype&equals;absolute

true

(3)

Compatibility

• 

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

• 

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

See Also

CodeTools[ProgramAnalysis][LoopInvariant]

CodeTools[ProgramAnalysis][VerifyLoop]

CodeTools[ProgramAnalysis][CreateLoop]

CodeTools[ProgramAnalysis]