Re: Ada 2012 Constraints (WRT an Ada IR)

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

On 13/12/2016 12:19, Dmitry A. Kazakov wrote:
> On 13/12/2016 11:39, G.B. wrote:
>> On 13/12/2016 09:27, Dmitry A. Kazakov wrote:
>>
>>>> No Ada in there. I was thinking of this posting.
>>>
>>> Ada is an object language here. Thus it can never be Ada. It could be
>>> a meta language of annotations for Ada, like SPARK.
>>
>> Pre doesn't have to be object language as has now been
>> said and confirmed a number of times.
>
> Being a part of the body it does not belong to declarations.

Right, Pre aspects are *not* body!  They have a right to
be part of some sort of monitoring program that observes
the first if they are to have an operational effect at all.
They are assertions separate from the program itself.

And they need *not* be exhaustive, even saying of what
would be hard, if possible at all. I think that is
agreement.

Whatever GNAT happens to do now does not change all this.

>>> It is an explicit contract.
>>
>> Can you make it a Boolean expression?
>
> That depends on the language in question. It is not an expression in Ada and cannot be made one.

Please, it's simple, actually, for what I had suggested,
a relation involving the two parameters A and B to be
passed to Plus_Too, since Standard.Integer is finite.

One lists inputs to Plus_Too as pairs that one specifies as not
mathematically overflowing the sum in Integer, for a start.
That's far from not expressible in Ada, it's not perfect
either, and it is highly inconvenient.

   (A => Integer'Last, B => Integer'Last)

will be a pair not listed,

   (A => -1, B => 42)

meets the requirements, and is listed.


>> So, what are expected values for various inputs of A and B
>> passed to Plus_Too? Can this be stated?
>
> Yes it can and it is already done by the provided implementation of Plus_Too.

It needs to be stated before the fact to be useful.

Without an implementation yet, one cannot infer its precondition.
But it is possible to write a predicate that is the specification
of a set of values from which some implementation is to compute
results.

> You keep on confusing program behavior with statements about it.

See above.


>> Gödel's results do not apply to "+" in Standard.Integer,
>> so nothing is due to them here.
>
> They apply to a framework capable to spell all preconditions of "+". No such thing can exist. Therefore some [most] contracts will remain implied forever.

I only asked for a relation between A and B as inputs to Plus_Too.
I cannot reasonably ask for an exhaustive Boolean expression that
makes the silly attempt to describe the universe of possibilities
in which Ada's "+" may have a number of effects.