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>:

• Any of the class members.

• Any of the global variables declared in every file where a method of the class (or a method of descendant if it is not a single class contract) is defined.

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

• Local variables of any methods.

• Macros: Global variables that are not defined in at least one file where a method of the class (or one of its descendants, if it is not a single class contract) is defined.

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);

}