On Fri, 16 Dec 2016, G.B. wrote:

> no statement of the Ada block
>
>  begin   -- of Make
>    ....
>  end Make;
>
> will execute "raise Constraint_Error" announced in Pre. In fact,
> RM 6.1.1(36/3) shows that Make cannot possibly raise the exception
> from inside, because then, technically, it could handle it there,
> contradicting the RM.
>
> So if "Post" means "After", then a contract violation may come
> first and an Assertion_Error is raised after that, but the
> execution of statements of Make will not have begun. So, in
> contract based design, Make does what it is supposed to do and
> does *not* check its Pre, just like proofs do not check their
> premises. (Eiffel just attaches names to "require"'s Boolean
> expressions, for reference.)

Well, follosing the Eiffel lead and Bertrand Mayer's writings, the client 
will not care where, exactly, the exception is raised. The client is 
calling the subprogram with certain values as parameters, and the client 
will get some expected result, even if it is a specific exception.

The else-clause still turns the Pre aspect into a postcondition.

On the other hand, Randy's point is quite convincing: If we want to 
introduce contracts -- and, specifically, preconditions -- into existing 
libraries without breaking compatibility, then the else clause is exactly 
what is needed.

So then the Pre-part of the contract essentially says:

    Don't call Make with First > Last!   -- This is a proper precondition.

    but your legacy code, which has been written before we fixed this
    contract, does not need to be rewritten.
    -- This is about software which still expects no precondition, but
    -- the old postcondition.

That makes sense!


--------  I  love  the  taste  of  Cryptanalysis  in  the morning!  --------
www.uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks
----Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany----