Go to the first, previous, next, last section, table of contents.


eiffel.h: eiffel type assertions

Eiffel is a very nice language which provides the assertion checking facilities of nana inside the language itself. The `eiffel.h' library is intended to provide a similar setup to Eiffel in the C++ language. It is a pretty poor emulation, but it is hopefully better than nothing.

Assertion checking is controlled by the EIFFEL_CHECK variable which can take on any of the following values:

CHECK_NO
Disable all checking.
CHECK_REQUIRE
Check the preconditions for each method.
CHECK_ENSURE
And also check the postconditions.
CHECK_INVARIANT
And also check the class invariant before and after each method is called. The programmer should provide a class method called `invariant' which returns `true' if the object is consistent, `false' otherwise.
CHECK_LOOP
And also check the loop invariants.
CHECK_ALL
And also check any assertions using the `CHECK' instruction.

A typical compile flag to the compile might be:

% g++ -c -DEIFFEL_CHECK=CHECK_ALL play.cc

And then we have the actual assertion macros.

Macro: void REQUIRE (exprn)
Called at the beginning of each method. This checks the precondition to a method and the class invariant.

Macro: void ENSURE (exprn)
Called at the end of each method. This checks the postcondition to a method and the class invariant.

Macro: void INVARIANT (exprn)
Used to check a loop invariant.

Macro: void CHECK (exprn)
Used for any other inline assertions.

And finally a small example:

#include <eiffel.h>

class example {
  int nobjects;
  map<location,string,locationlt> layer;
public:
  bool invariant();
  void changeit(location l);
};

bool example::invariant() {
  return AO(i,layer,valid_location((*i).first)) && 
         nobjects >= 0;
}

void example::changeit(string n, location l) {
  REQUIRE(E1O(i,layer,(*i).second == n));
  ...;
  while(..) {
    INVARIANT(...);
    ...
    INVARIANT(...);
  }
  ...
  CHECK(x == 5);
  ...
  ENSURE(layer[l] == n);
}

Note that the invariant checking macro `example::invariant' is called automatically on function entry/exit using the `REQUIRE' and `ENSURE' macros.


Go to the first, previous, next, last section, table of contents.