Assertions are expressions that must be true before and after a method is executed. For example, the method

     proc push( x : integer )
         before not full();
         var oldSize : integer = getSize();
         after  not empty() and oldSize == getSize() - 1;
     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.

What is new ?

    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.