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.