Re: about the new Ada 2012 pre/post conditions

[Simon Wright <simon@pushface.org>]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> 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.

If a DbC program passes a negative argument to sqrt(), then it isn't
correct.

To prove that a DbC program never passes a negative argument to sqrt()
requires a proof (tautology).

No proof is required of the statement that a correct program must not
pass a negative argument to sqrt() - the contract must be regarded as
axiomatic from the caller's pov.

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

I can't make sense of this statement.

> 3. While you are busy proving 1 and 2, I'd rather stay on the safe side
> considering sqrt (-1.0) happen. So, what about the effect?

There will be an exception. What's the problem with that?

In my last project, unhandled exceptions caused the system to be
rebooted (and missiles in flight to be aborted). If the system throws an
unhandled exception it's operating outside its design envelope and
safety considerations come in to play.