Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

On 06.07.12 11:01, Dmitry A. Kazakov wrote:
> On Fri, 06 Jul 2012 10:30:01 +0200, Georg Bauhaus wrote:
> 
>> On 06.07.12 10:05, Dmitry A. Kazakov wrote:
>>> On Fri, 06 Jul 2012 09:41:18 +0200, Georg Bauhaus wrote:
>>>
>>>> On 05.07.12 21:55, Dmitry A. Kazakov wrote:
>>>>> On Thu, 5 Jul 2012 12:11:57 -0700 (PDT), Adam Beneschan wrote:
>>>>>
>>>>>> On Thursday, July 5, 2012 12:48:30 AM UTC-7, Dmitry A. Kazakov wrote:
>>>>>>
>>>>>>> Putting it even simpler. What is the effect of:
>>>>>>>
>>>>>>>      sqrt (-1.0)
>>>>>>>
>>>>>>> No effect? Any effect?
>>>>>>
>>>>>> This looks like an imaginary problem to me, not a real one.
>>>>>
>>>>> What problem? It was a simple question illustrating absurdity of the idea.
>>>>
>>>> Actually, a negative argument passed to sqrt is illustrating proper DbC
>>>> well. One famous example is Ariane 4, (4), that's the number four.
>>>
>>> If sqrt (-1.0) has no effect,
>>
>> First, in a DbC correct program, sqrt(r) where r < 0.0 does not occur.
> 
> 1. That no correct program may have it requires a proof.

Yes, this is why DbC is associated with a proof obligation.

> 2. That no program at all may have it, requires yet another proof.

Who cares? I mean, really, who cares?

Assertion checking is *not* the same as showing that there exists
a class of programs written in a suitably restricted language
that is free of a number of possible errors. It is about
programmers expressing things not expressible in Ada's type
system.

And DbC is about two parties, not just one.

> I'd rather stay on the safe side
> considering sqrt (-1.0) happen. So, what about the effect?

If you know that you might be running an incorrect program,
the effect is similar to that of using Unchecked_Conversion.


>>> what made Ariane to explode?
>>
>> The engineers though the didn't have to re-read the contract
>> for Ariane 4 when moving the software to Ariane 5.
> 
> But that has no effect or else does not occur... thus it never exploded.

"That" = the contract?

If a program is correct, then checking contract clauses does
not have adverse effects. If a program is incorrectly calling
sqrt with a negative argument, there are two practical cases

1) [wrong -1.0 and checks on] detects violation, restarts if possible

2) [wrong -1.0 and checks off] whatever sqrt's body does

Both situations can make the system crash, because it might
not be possible to retry using another, fresh value for r
in case 1). Some have expressed a preference for detection (1) over
erratic performance (2).

I'll note in passing that a check is *not* testing I/O values.
By the Ariane analogy, the original *system* was assumed, correctly,
to guarantee that r >= 0.0. But another, different assembly of
a new system rendered the guarantee void, introducing an explosive bug.