4.14.2 DOEND: adding DO ... END

At the suggestion of Bertrand Meyer (Eiffel's author) the DO and END macros have been added to `eiffel.h'. Note that these are only available if you define the EIFFEL_DOEND macro. To use these macros each of your methods should use DO ... END as their outermost brackets. For example:

     // compiled with EIFFEL_DOEND defined
     void Stack::push(int n)
     DO  // checks the class invariant + {
        ...
     END // check the class invariant + }

If you do not define the EIFFEL_DOEND macro then `eiffel.h' reverts to its old behaviour where `REQUIRE' and `ENSURE' also check the class invariant. Thus to check the class invariant when you are not using DO and END you would need to call REQUIRE and ENSURE, for example:

     // compile with EIFFEL_DOEND undefined (i.e. old behaviour)
     void Stack::push(int n)
     {
       REQUIRE(true); // checks the invariant as well as the precondition
     
       ENSURE(true); // checks the invariant as well as the postcondition
     }

As for which one to option to pick, Bertrand Meyer is in favour of the DO ... END solution.