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.