Re: Ada 2012 Constraints (WRT an Ada IR)

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

On 15/12/2016 11:31, G.B. wrote:
> On 15/12/2016 09:41, Dmitry A. Kazakov wrote:
>> In Ada type declarations must be there, so it is not a tool, but an
>> integral part of the language. This is why "pre"-aspects is a
>> non-starter even ignoring their semantic consistency issues. You can
>> do things with or without them. Psychologically it won't work.
>
> Problem statement:
> Devise a type that represents an ordered pair of linearly
> ordered numbers, such that programmers can create objects that
> have the two elements in proper order.

It is a good illustration of what is wrong with ideas you promote. You 
are thinking in terms of implementations.

Ada, at least Ada 83 was focused on ADT and designed to be language that 
supporting software design in terms of ADTs as opposed to loose data 
structures.

An Ada programmer would rather design an integer interval type than data 
structure you described. Whether he would choose a pair of interval 
bounds to represent it, or the lower bound and length, or whatever else 
he would not expose it in the declarations.

Neither there is any reason to derive an interval type from a pair and 
put a constraint on the pair as you seem suggest. That is an 
implementation. Semantically pairs and intervals are not related types.

Then lower<=higher is not a constraint, it is an invariant, if any. 
Furthermore from the correctness proofs standpoint the post-conditions 
of interval arithmetic trivially ensure the invariant. E.g.

    [a,b] + [c,d] = [min(a,b), max(c,b)]

So there is no need to spell the invariant. And finally, invariant is an 
implementation detail not to expose anyway.

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