Assertions are expressions that must be true before and after a method is executed. For example, the method
proc push( x : integer )
assert
before not full();
var oldSize : integer = getSize();
after not empty() and oldSize == getSize() - 1;
end
begin { method body }
...
end { push }
of a class Stack defines a pre-condition "not full() " and post-condition "not empty() and oldSize() == getSize() - 1". Between before and after there may appear declaration and initialization of variables used in the after part. "full" and "getSize" are public methods of class Stack − they must be public.
If the before or after expression evaluates
to false, an exception AssertionBeforeException or AssertionAfterException
will be thrown. These two exception classes inherit from AssertionException.
Nothing
that cannot be simulated in language Eiffel, although the syntax is very convenient.
The declaration of variables between clauses before
and after is new and was designed to replace the use of the old keyword of Eiffel. The hierarchy of AssertionException is new and allows the programmer to catch all
exceptions caused by assertions or just the exceptions caused by the before (or after) clause.
An object of a catch class that has only one method
proc throw( exc : AssertionException )
will catch all assertion exceptions. If the
catch class had method
proc throw( exc : AssertionBeforeException )
the object would catch only exceptions caused by
the before clause.