The PRE_CONDITION and POST_CONDITION Statements

The PRE_CONDITION and POST_CONDITION assertion statements are modeled after the ASSERT statement provided in the C language. They are used to check the value of variables at the point of method/function entry and exit respectively. A PRE_CONDITION is evaluated as the first statement of a method/function. A POST_CONDITION is evaluated as the last statement of a function/method before the return statement (or end of the function, if no return statement is provided). If multiple return statements exist, then the POST_CONDITION will be evaluated before whichever return statement is reached.

Both PRE_CONDITION and POST_CONDITION statements may be used as either Definition Placed assertions or Specification Placed assertions. When used as a Definition Placed assertion, a PRE_CONDITION or POST_CONDITION should be placed immediately after the opening ``curly brace'' of a function/method. POST_CONDITIONs will be evaluated at the proper place in the function/method despite their location at the top of the function / method definition. An example of a Definition Placed PRE_CONDITION and POST_CONDITION is:

void
Screen::LightPixel(int x, int y)
{
  PRE_CONDITION ((x >= 0) && (y >= 0)), "Negative screen coordinate given") ;
  POST_CONDITION( screen[x][y] == true, "Failed to light pixel") ;

  screen[x][y] = true ;
  return ;
}

The above example is equivalent to writing the following:

void
Screen::LightPixel(int x, int y)
{
  ASSERT((x >= 0) && (y >= 0)), "Negative screen coordinate given") ;

  screen[x][y] = true ;

  ASSERT( screen[x][y] == true, "Failed to light pixel") ;
   return ;
}

The same PRE_CONDITION and POST_CONDITION statements could be written as Specification Placed assertion statements (for C++ only), and they would be evaluated identically. Specification Placed assertion statements are written as:

class Screen
{
  private:
     bool screen[10][10] ;

  public:
    LightPixel(int x, int y) ;
      PRE_CONDITION((x >= 0) && (y >= 0)), "Negative screen coordinate given") ;
      POST_CONDITION( screen[x][y] = true, "Failed to light pixel") ;
    ClearPixel(int x, int y) ;
}