C++ Test Script Language


TRANSITION <state name> TO <state name>;




The TRANSITION statement describes a transition between two states an object can execute during its life.

<state name> is a valid state name defined with the STATE keyword.

Transitions are checked between two state evaluations. States are evaluated at the end of the execution of class constructors (except for implicitly-defined copy constructor), at the beginning of class destructors, and both at the beginning and the end of other non-static non-implicitly defined methods.

All states are evaluated after an object has been created (when leaving a constructor). Consequently, the initial state must be described in a non-ambiguous way: one - and one only - state must occur when leaving a constructor.

Once a state has been determined, only authorized states (according to the defined transitions) are checked. Ambiguity must not occur when choosing the next state.

States are always reflexive. This means that a transition from a state to itself is implicitly defined. There must be no ambiguity between one state and any other state that can be reached through a single transition.


C++ source code example:

class Stack {

       int count;

       int capacity;

       Stack () : count(0) {}

       void push (void *);

       void *pop ();



C++ Contract Check Script code example:

CLASS Stack {

       STATE Empty { (count == 0) }
STATE NotEmpty { (count > 0) (count < capacity) }
STATE Full { (count == capacity) }

       TRANSITION Empty TO NotEmpty;

       TRANSITION NotEmpty TO Full;

       TRANSITION Full TO NotEmpty;

       TRANSITION NotEmpty TO Empty;