Re: Renaming Fixed Point Mutiplicative operator in Ada 95

["Stuart Hutchesson" <shutch@innotts.co.uk>]

Robert Dewar <dewar@merv.cs.nyu.edu> wrote in article
<dewar.895785693@merv>...
> 
> 
> Incidentally, in a critical system, I would jolly well hope that EITHER
> 
>  a) you prove that division by zero cannot happen
> 
> or
> 
>  b) you test for it explicitly
> 
>     if z = 0 then
> 	....
>     else
>         a := y /z;
>     end if;
> 
If you are suggesting that all divisions are guarded by a test for
denonimator non-zero - then wouln't the most obvious place for that test be
within the division operator itself! Otherwise you have a massive
review/verification effort to check that all divisions are guarded! If it
is inside the operator then that test is done once.  Also
 there is the question of the code that has to be placed inside the "if"
side of the check.

Plus you have to consider all the other guards that have to be placed
around both multipy and divide operations for overflow of the destination
type etc.  The neatest and most cost-effective solution is to put them
inside an overridden operator.

(BTW - the example you gave in your previous posting of surrounding the
operation with an exception handler is banned by SPARK Ada.....)