Here are the individual checking macros:
Called at the beginning of each method to check its precondition (requirements). For example:
void Stack::push(int n) { REQUIRE(!full()); // stack has space for push ... }If
EIFFEL_DOEND
is not defined this also checks the class invariant.
Called at the end of each method. This checks the postcondition for a method and the class invariant.
void Stack::push(int n) { ... ENSURE(!empty()); // it can't be empty after a push! }If
EIFFEL_DOEND
is not defined this also checks the class invariant.
Used for any other inline assertions. For example:
CHECK(z != 0); x = y / z;
And finally a small example:
#include <eiffel.h> class example { int nobjects; map<location,string,locationlt> layer; public: bool invariant(); // is this object consistent 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 if ‘EIFFEL_CHECK’ is not defined.