peter horan

I have just verified that you are right (using EiffelStudio 5.4). The
invariant is checked before the precondition. A broken invariant means
that a potential user must not touch the object for any purpose. It can
only be rescued in the client.
--
Peter Horan School of Information Technology
peter@deakin.edu.au Deakin University
+61-3-5227 1234 (Voice) Geelong, Victoria 3217, AUSTRALIA
+61-3-5227 2028 (FAX) http://www.cm.deakin.edu.au/~peter

-- The Eiffel guarantee: From specification to implementation
-- (http://www.cetus-links.org/oo_eiffel.html)