REQUIRE... - Untitled

4.14.3 REQUIRE, ENSURE, CHECK, etc.

Here are the individual checking macros:

— Macro: void REQUIRE (exprn)

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.

— Macro: void ENSURE (exprn)

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.

— Macro: void INVARIANT (exprn)

Used to check a loop invariant.

— Macro: void CHECK (exprn)

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.