INVARIANT

C++ Test Script Language

Syntax

INVARIANT <native expression>;

Location

CLASS

Description

The INVARIANT statement describes a condition that should be always true in an object life, that is, whenever one of its method can be called. It appears in a CLASS block.

<native expression> is a C++ Boolean expression (or an expression that can be converted to a Boolean).

The following symbols can be used in <native expression>:

The following symbols cannot be accessed in <native expression>:

Evaluation:

<native expression> is evaluated at the end of the execution of the class constructors (except the implicitly defined copy constructor), at the beginning of the class destructors, and both at the beginning and the end of other non-static non implicitly defined methods.

Warning: You can call methods in <expr>, but you must ensure that these calls do not modify the object's state (that is, they do not write to any field). You can ensure this by calling const methods only. If you want the compiler to check this, see the ATO_AC_STRICT_CHECKING Target Package option.

Example

C++ source code example:

class Stack {

       int count;

       Stack () : count(0) {}

       void push (void *);

       void *pop ();

};

 

C++ Contract Check Script code example:

CLASS Stack {

       INVARIANT (count >= 0);

}