Re: Contracted exceptions for Ada

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

On Mon, 10 Dec 2007 20:25:34 +0000, Simon Wright wrote:

> The Ariane IV system engineers said to themselves, and probably in the
> design documentation, "The maximum horizontal velocity is X. Therefore
> the conversion to the fixed-point type _Whatever_ cannot
> overflow. Therefore we do not need to handle exceptions for this
> conversion, so (given we are short of CPU power) we will not do any
> extra processing to avoid exceptions."
>
> Not sure they would have recognised "contract" in that context.

Yes, my premise was that the type of H_Input changed from Ariane IV to
Ariane V. In this case translation of the conversion function
H_Input_To_Whatever could refute the second "therefore" because X would not
be the maximal possible value of H_Input anymore.

>> 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... (:-))
> 
> Not if there was no port, and the exact same hardware with the exact
> same software was reused! (I'm not sure if that was in fact the case)

You mean that the ADC was reused as well? In that case (just speculating of
course) the compiler could detect the problem already for Ariane IV,
noticing that the range of H_Input is not bound by X and forcing to add an
exception handler somewhere.

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