Re: Division by zero

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

On Sun, 12 Jun 2005 21:43:16 +1200, Lurker wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:79ahr0jozmqb$.10jzllrcjpmsv.dlg@40tude.net...
> 
>>> Well, yes. But can't it tell that division by zero is always wrong
>>> regardless?
>>
>> No, it is not, because it has a defined effect: Constraint_Error. Formally
>> speaking division by zero is not a contract violation and thus cannot be
>> "wrong". Consider the following:
>>
>>    A : constant Integer := 0;
>>    B : Integer := 1;
>> begin
>>    B := B / A;
>>    Put_Line ("Hello!");
>> exception
>>    when others =>
>>       Put_Line ("Good bye!");
>>
>> The above is a valid program, which should print "Good bye!". At the same
>> time the following is *wrong*:
>>
>>    A : constant Integer := 0;
>>    B : constant Integer := 1;
>>    C : Integer;
>> begin
>>    C := B / A;
>>
>> B/A is a static expression, which has to have a value at compile-time.
> 
> OK, I see you point. But, pratically speaking, the chances are that
> that construct was an error. Perhaps a warning or some such would
> be enough. If whoever wrote that was sure that's what they meant - fine.
> But I was always under the impression that the Ada philosophy was
> to avoid accidental mistakes as much as possible. And division by
> zero sure should qualify as a suspect at least - not something that
> just happily gets compiled.
> 
>>>> Constraint_Error will be raised at runtime.
>>>
>>> It was. My question was - should it have been caught
>>> at compile time instead?
>>
>> I don't think it should. A class of errors which cannot be detected at
>> compile time cannot be compile-time errors. Or, in other words, if you
>> cannot rely on the compiler, you should not pretend you can. (:-))
> 
> I'm afraid I don't follow your logic there. Do you really mean that
> a constant declared as = 0 cannot be detected at compile time?
> 
> Yes, the effects of using it to divide something may or may not be ok.
> But that would equally apply to dividing a literal 1 by it, wouldn't it?
> 
> (Again, I realise your point about static vs other expressions.
> But c'mon, unless someone specifically allows and handles
> cases like that, surely the safest bet would be to at least point
> out that there is something fishy going on and a "moral equivalent"
> of asking "are you sure"?

The problem is in classification of this error (see also ARM 1.1.5):

1. language errors
2. run-time errors
3. bounded errors
4. logic errors

You cannot require zero-divide be in 1 for obvious reasons. So it is in 2.
The case of fully static expressions can be in 1 (and is), because static
expressions are handled at compile-time.

Now, if you want to bring <anything>/0 to the class 1, you should provide a
carrier in the language to formulate it. The only one available in my view
(let the language lawyers step in) is the type system. So a possible way
could be "statically valued" types. Then you would be able define:

function "/" (Left, Right : T) return T;
   -- This raises Constraint_Error (class 2)

function "/" (Left : T; Right : static T) return T;
require (Right /= 0);
   -- This gives a compile error (class 1), yet I can re-define it and
   -- implement, say, IEEE-like semantic of zero-divide

Note, that the semantic of / can be re-defined. So in general case, even if
0 is static, the compiler cannot deduce that X/0 is an error without
looking into the implementation of /. That's a halting problem. Therefore
the only way I see, is a typed one, i.e. "statically valued" types.

This step, or something similar, would have very serious consequences
difficult to predict. In any case it would be not easy to do.

If you ask for my opinion, then yes, I would like to have more influence on
[partially] static expressions and the way one could ensure that something
(complex) be evaluated at compile-time. But I bet that there are lot of
people who want the opposite.

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