Re: Ada 2012 Constraints (WRT an Ada IR)

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

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.


>>> Implied contracts are outside the scope.
>>
>> My point. Why should contracts not be explicit, in particular
>> when they had already been formal, albeit in a comment?
>
> Explicit contracts are only ones the framework can enforce, at all or pragmatically.

Which role do programmers play in this? Are frameworks so much
better at proving and enforcing than humans? They are man made
frameworks after all, so whether they should necessarily limit
the scope of man seems dubious.


> It is an explicit contract.

Can you make it a Boolean expression?

> The contract gets violated when the Plus_Too does not return expected value due to consumption of the CPU by the black hole.

So, what are expected values for various inputs of A and B
passed to Plus_Too? Can this be stated? Partially? I do think so.

>> (Actually, there is no variable in the predicate other than those
>> implied in sub-expressions of Earth turning a black hole.
>
> Your fault. Formally no such predicate could even exist, merely due to Goedel incompleteness.

Gödel's results do not apply to "+" in Standard.Integer,
so nothing is due to them here.

> There is an old programmer's saying: never check bugs you are not going fix...

Which is reflected in the saying that a failed Pre check
puts some bug directly under my nose, and that's by intent.

No proof can show bugs' absence whenever there is no predicate
describing expected values.