Re: Contracted exceptions for Ada

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Sun, 09 Dec 2007 18:39:31 +0000, Simon Wright wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> On Sun, 09 Dec 2007 16:11:13 +0100, Martin Krischik wrote:
>>
>>> Dmitry A. Kazakov wrote:
>>> 
>>>> (Maybe a wild guess, but this could save Ariane V. A program assumed
>>>> Constraint_Error exception free was recompiled for the hardware where that
>>>> was not the case.)
>>> 
>>> My understanding is that the system was brought down by an unexpected
>>> hardware exception - i.E. one which the CPU's floating point unit
>>> generated.
>>
>> Yes, and that would be detected by the compiler:
>>
>>    function Integer (X : Float) return Integer;
>>
>> which was contracted as exception-free on one platform will not be on
>> another. So the compiler would reject either its implementation that raises
>> Constraint_Error or else its use contracted as Constraint_Error-free. So
>> the idea.
> 
> I don't see how the compiler/platform in use has anything to do with
> this.
> 
>     In Ariane IV the maximum horizontal velocity is X.
> 
>     Therefore we can convert the hardware input to this-type without
>     worrying about overflow.

Hardware input had a type different from one used later in the control
circle, because it needed to be converted. So what was the contract of that
conversion?

>     Therefore any exception will be caused by hardware error.

The article mentioned by Martin talks about floating point to integer
conversion. Was the conversion programmed in Ada? Probably it wasn't. Then
I can only wonder why people keep on talking about "Ada fault"...

> seems a proper analysis for Ariane IV; reusing precisely the same
> software/platform in an environment where the maximum horizontal
> velocity was much larger than X is an error that no amount of
> *software* engineering is going to fix.

My point is that the fault could be detected (assuming that conversion was
in Ada), under the condition that the compiler vendor would not make the
same mistake while porting the compiler... (:-))

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de