Re: Ada 2012 Constraints (WRT an Ada IR)

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

On 15/12/2016 14:17, Dmitry A. Kazakov wrote:
> 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.

Am I?  ;-)

In any case, I wasn't thinking of arithmetic at all. Maybe graphs'
edges. But certainly I had the simple concept of an order pair in mind.

Trying to follow your advice, though, with Post for emphasis,
lets see how well the type works without Pre.

    type Immutable_Ordered_Pair (<>) is private;

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

    function First (Pair : Immutable_Ordered_Pair) return POT;
    function Second (Pair : Immutable_Ordered_Pair) return POT;

Type POT has "<=", its name suggesting a partially ordered set.
The full view of Immutable_Ordered_Pair carries a hidden

    Type_Invariant => First <= Second;

naming obvious components, and it is hidden in the private part
as requested.

Now what will (*) yield if uncommented, thus ignoring your advice?
First, this is what Make could do without a Pre aspect:

   - raise some X_E if "<=" can raise X_E;

   - handle X_E and reorder the parameters ("At your service!")
     and retry, noting the attempt and raise X_E if "<=" does it
     again, otherwise return a pair made form the parameters reversed;

   - an unnecessary check in case the programmer passes First and
     Second properly ordered, i.e. (First <= Second) = True.

Now give the programmer Pre as it follows from {Post, Type_Invariant},
and you are designing by contract:

   - Make assumes Pre is true, so it simply returns a new object,
     since its assumption, Pre, entails {Post, Type_Invariant}.

It is contract violation if the programmer has passed values
not in "<=", violating Pre, so Make will not create and object.

Simple, no secrets, consistent, and efficient.

As opposed to:
Not Simple, arcane, consistent, and inefficient.

The reversal of parameters in the body of the rather complex Make
(when Pre is undisclosed) could instead be made a service procedure
or constructing function. For variables:

    procedure Swapped_As_Necessary (X, Y : in out POT)
    with
      Pre => True,
      Post => (if X'Old <= Y'Old
               then X = X'Old and Y = Y'Old
               else X = Y'Old and Y = X'Old);

But whenever an algorithm already has Post => x < y, then there
is no need to use that service procedure. Just call Make (x, y),
it is safe WRT contracts. Rest assured that Make won't raise A_F
and instead will produce objects as desired, and quickly.