Re: Ada 2012 Constraints (WRT an Ada IR)

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On 2016-12-11 12:21, G.B. wrote:
> On 09/12/2016 10:38, Dmitry A. Kazakov wrote:
>> On 08/12/2016 19:35, G.B. wrote:
>>> So, the following function will also just announce that
>>> it can raise Constraint_Error?
>>>
>>> function Plus_Too (A, B: Standard.Integer)
>>>                   return Standard.Integer is
>>> begin
>>>    return A + B;
>>> end Plus_Too;
>>
>> At least. Contracts have different precision of the post-condition:
>>
>> 1.    Constraint_Error
>>    or none
>>
>> 2.    Constraint_Error when combination of argument values
>>    or none
>>
>> 3.    Constraint_Error when combination of argument values
>>    or 0 when combination of argument values
>>    or 1 when combination of argument values
>>    ...
>
> So, what is it, and (not?) elevated to implementation in this case
> of Plus_Too?

?

> McJones and Stepanov show an example which, I think, is related[1,2].
> Note the precondition.

It is not.

> T remainder(T a, T b)
> {
>    // precondition a ≥ b > 0
>    if (a - b >= b) {
>       a = remainder(a, b + b);
>       if (a < b) return a;
>    }
>    return a - b;
> }
>
> "... requires thinking."
>
> They move towards Correctness, introducing, IIUC, a (finite) semi-group
> of integers with both a 1 and Archimedes' axiom, < total, ... T a
> QuotientType
> (I won't guess what the latter is, but will guess that some here might
> know that).
>
> And, a precondition is stated as a comment, but the caller doesn't know it
> unless he or she studies the body! Not the specification.
> Granted, the programming language they use is a small language made for
> a book, and the precondition is given on the first line. But if the language
> were based on Ada, shouldn't it become a Pre aspect,
>
>    function Remainder (A, B : T) return T
>       with Pre => A >= B and B > 0, ...;

To be a proper precondition it must be SPARK, not Ada.

An expression evaluated in the program is never a precondition. Pre-, 
post-, invariants are expressions evaluated by the *prover*. They are in 
the language of *prover*, they are *not* statements of the object language.

 > so that the caller
 > knows what to do about a and b and the implementation of `remainder`
 > can assume it's been done?

That does not translate to me into anything.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de