Re: Ada 2012 Constraints (WRT an Ada IR)

["G.B." <bauhaus@notmyhomepage.invalid>]

On 16/12/2016 11:04, Dmitry A. Kazakov wrote:

>>    function Make (First, Second: POT) return Immutable_Ordered_Pair
>>    with
>>      --Pre => First <= Second,   -- (*)
>>      Post => Make'Result in Immutable_Ordered_Pair; -- or raise
>
> Right, no precondition

As you have chosen to not address, except for here saying
"no precondition" while stating a Pre later, the lack of Pre
will cause major differences. They comprise both Make
and the whole design and efficiency, all as outlined.
How could anyone always ignore these differences?

>> Now give the programmer Pre as it follows from {Post, Type_Invariant},
>> and you are designing by contract:
>
> No. Pre does not follow from Post. The one that does is different:
>
>    First >= Second or else Constraint_Error is propagating

I assume you meant

     First <= Second or else Constraint_Error is propagating?

Which is basically the observable behavior of current Ada,
except that

- with Pre,
     a call may have been started, but is stopped from entering
     the Ada-body,

- without Pre,
     the Ada-body has started checking and runs into all sorts
     of decisions, and possibly into the Type_Invariant not
     being True for the parameters it has already "accepted".

> The key difference is

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

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?

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