The INVARIANT Statement

An INVARIANT statement is a combination of the PRE_CONDITION and POST_CONDITION statements. It is used to check that a condition holds at both the beginning and end of every public method in a class. It is equivalent to writing both a PRE_CONDITION and POST_CONDITION for each public method. In a constructor or destructor, it acts as only a POST_CONDITION or PRE_CONDITION respectively. An INVARIANT statement must be placed in the specification of a class, and this feature is only available in the C++ capability of ASSERT++. The statement is placed immediately after the opening ``curly brace'' at the beginning of a class specification. An example of an INVARIANT statement is:

class Screen
{
  INVARIANT( (cursorX > 0) && (cursorY > 0), "Negative coordinate given") ;
  private:
     bool screen[10][10] ;
     int cursorX ;
     int cursorY ;

  public:
    LightCursor(void) ;         // Lights up the current cursor position
}

This is equivalent to writing:

class Screen
{
private:
     bool screen[10][10] ;
     int cursorX ;
     int cursorY ;

  public:
    LightCursor(void) ;         // Lights up the current cursor position
      PRE_CONDITION( (cursorX > 0) && (cursorY > 0), 
                     "Negative coordinate given") ;
      POST_CONDITION( (cursorX > 0) && (cursorY > 0), 
                     "Negative coordinate given") ;
}