Next: REQUIRE..., Previous: EIFFEL_CHECK, Up: eiffel.h
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.