CodeTools[ProgramAnalysis] - Maple Programming Help

Online Help

All Products    Maple    MapleSim


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

CodeTools[ProgramAnalysis]

  

VerifyLoop

  

verify if a WhileLoop satisfies its post-condition

 

Calling Sequence

Parameters

Options

Description

Examples

Compatibility

Calling Sequence

VerifyLoop(loop, invariant, options)

Parameters

loop

-

WhileLoop

invariant

-

boolean function; invariant of loop

options

-

(optional) sequence of equations, as listed in the Options section below

Options

• 

checkinvariants = false (default) or true

  

Specifies whether or not the invariant invariant should be checked using IsLoopInvariant

• 

invarianttype = plain, inductive or absolute

  

Specifies the type of invariant check to be performed on invariant, either a plain invariant, an inductive invariant or an absolute invariant

• 

output = truefalse (default) or counterexample, or a list thereof

  

Specify the command's output.  By default, the command returns a truefalse value stating whether or not the post-condition holds.  When counterexample is given, a list with the polynomial ring RegularChains[PolynomialRing] of the system and a sub-list of regular semi-algebraic systems that violate the post-condition is returned (see the SemiAlgebraicSetTools package for details on working with regular semi-algebraic systems).  The counter example will be the empty set (represented by an empty list) when loop is guaranteed to satisfy its post-condition.

Description

• 

This command verifies whether or not loop's post-condition is true given its pre-condition, the negation of its guard condition and the loop invariant inv.  The pre-, post- and guard conditions were all extracted from the ASSERT statements in the original procedure when CreateLoop was called.

Examples

withCodeTools[ProgramAnalysis]:

The following procedure computes the square root of a positive number to within the given tolerance err. The ASSERT statements contain the pre- and post-conditions of the loop, which is considered to be the specification of the loop.

z3sqrt := proc (a, err)
    local r, q, p;
    r := a - 1;
    q := 1;
    p := 1/2;
    ASSERT(a <= 4 and 1 <= a and 0 < err and p > 0);
    while err <= 2 * p * r do
        if 0 <= 2 * r - 2 * q - p then
            r := 2 * r - 2 * q - p;
            q := q + p;
            p := 1/2 * p:
        else
            r := 2 * r;
            p := 1/2 * p:
        end if:
    end do;
    ASSERT(q^2 <= a and a < q^2+err);
    return q:
end proc;

z3sqrtproca&comma;errlocalr&comma;q&comma;p&semi;ra1&semi;q1&semi;p1&sol;2&semi;ASSERTa<=4and1<=aand0<errand0<p&semi;whileerr<=2&ast;p&ast;rdoif0<=2&ast;r2&ast;qpthenr2&ast;r2&ast;qp&semi;qq&plus;p&semi;p1&sol;2&ast;pelser2&ast;r&semi;p1&sol;2&ast;pend ifend do&semi;ASSERTq&Hat;2<=aanda<q&Hat;2&plus;err&semi;returnqend proc

(1)

Construct the WhileLoop data structure:

loopCreateLoopz3sqrt

loopRecordWhileLoop&comma;variables&equals;p&comma;q&comma;r&comma;parameters&equals;a&comma;err&comma;initialization&equals;12&comma;1&comma;a1&comma;transitions&equals;02r2qp&comma;12p&comma;q&plus;p&comma;2r2qp&comma;&comma;12p&comma;q&comma;2r&comma;guard&equals;err2pr&comma;precondition&equals;a4&comma;1a&comma;0<err&comma;0<p&comma;postcondition&equals;q2a&comma;a<q2&plus;err&comma;returnvalue&equals;q

(2)

Compute the absolute invariants of loop:

invariantLoopInvariantloop&comma;invarianttype&equals;absolute

invariant2pr&plus;q2a&equals;0

(3)

The verification of the loop fails in this case because the pre-condition is not strong enough:

verification_counter_examplesVerifyLooploop&comma;invariant&comma;output&equals;counterexample

verification_counter_examplespolynomial_ring&comma;regular_semi_algebraic_system&comma;regular_semi_algebraic_system&comma;regular_semi_algebraic_system&comma;regular_semi_algebraic_system&comma;regular_semi_algebraic_system

(4)

The RegularChains:-Display command can be used to see what values of the loop variables violate the post-conditions:

RegularChains:-Displayverification_counter_examples21&comma;verification_counter_examples1

&lcub;a2rpq2=02rp+q24=0q<−2anderr>0andr<0andq2+err40

(5)

The pre-condition did not include that r is always positive.  Supplying this piece of information in addition to the computed invariant allows us to verify that post-condition is satisfied:

VerifyLooploop&comma;Andinvariant&comma;0r

true

(6)

This means that the condition in the ASSERT statement at the end of z3sqrt will indeed always return true and that the square root will be within the desired accuracy.

Compatibility

• 

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

• 

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