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

> ... a design choice: establishing the precondition is work
> to be done be the programmer who writes the call. There may be
> Make'Pre as a guide. If there isn't, the implementers of
> Make and writers of Make'Post have not done their homework.

Make'Pre isn't just a guide, it is a contract. ;-)

> But this is puzzling:
> Suppose the compiler can't prove that calling Make is safe in the
> Pre/Post sense. Then, how did the programmer of Make determine
> which parameters will lead to safe return? And be silent about it?

Technically, the programmer is responsible for *never* violating the 
precondition, ever. That is the whole point of a *precondition*.

So First <= Second is a proper precondition, telling the customer to 
never, ever call Make with First > Second:

    function Make (First, Second: POT) return Immutable_Ordered_Pair
    with
      Pre => First <= Second,
      Post => ...

In contrast, the notation with "or else Exception" is technically not a 
precondition, any more. It tells the reader/client: "You don't need to 
bother with the order of First and Second. If you call Make with First > 
Second, I will raise a specific exception that you may handle, then.":

    function Make (First, Second: POT) return Immutable_Ordered_Pair
    with
      Pre => First <= Second or else Raise_Constaint_Error,
      Post => ...

While Ada writes this conveniently as a precondition, it actually is a 
postcondition. Dmitry is right at that point.

Now, I am not as dogmatic as Dmitry sometimes is. Sure, the "or else 
Exception" notation is a minor abuse of the "Pre" aspect, and the "Post" 
aspect would have fitted better. But this is just a marginal syntactic 
issue, and having the option to specify the specific exception is great!

> Again, I think that an important purpose of the Pre aspect is to
> inform the programmer about when *not* to call.

Well, that is the purpose of a precondition, but we have to live with the 
fact that the "Pre" aspect is also used for certain postconditions. Else 
something like

      Pre => First <= Second or else Raise_Constaint_Error,

would not make any sense at all!

If you never call the subprogram with First > Second, it will not raise 
the exception. And if the exception is not raised, anyway, then why, on 
earth, whould you care which exception is not raised?


A related but different point: Some people go even further and claim that

      Pre => First <= Second,

is not a proper precondition, because this is, de facto, the shorthand for

      Pre => First <= Second or else Assertion_Error.

I am afraid, that argument leads eventually into madness. If the compiler 
cannot prove that a certain call does not violate the contract, and if the 
programmer actually violates the contract, it makes sense to write some 
diagnostic information to somewhere and then shut down. Of course, 
handling Assertion_Error and then continuing, instead of shutting down, 
may be express route into madness. ;-)



--------  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----