Re: next "big" language?? (disagree)

[dewar@cs.nyu.edu (Robert Dewar)]

Brian says (regarding the possible interpretations of Assert):

  I'm not sure I see the complete distinction.  Wouldn't it be possible
  for a compiler to eliminate any divide-by-zero check from the
  following code sequence:
  
    if not (X /= 0) then
      raise Assert_Error;
    end if;
    Q := 30 / X;
  
  The divide is unreachable when X = 0.  Now this admittedly does
  cause a change in the generated code when an assertion is used.
  I'm trying to understand the "assertions should not affect things"
  camp.

It's delicate, but let's extend the example:

   Q := 30 / X;
   assert X /= 0;
   Q := 30 / X;

roughtly the three points of view are:

  1. the assert has no effect on the code, so the semantics is exactly
     equivalent to what you would get by leaving out the assert, but
     the assert can be checked at run time. In this model it would be
     wrong for the compiler to leave out the second divide by zero
     check. Warning: this model is hard to define formally.

  2. The assert is equivalent to an if. In this case the compiler can
     omit the second divide by zero check. This is what GNAT does, and
     is easy to define formally, since it is just an equivalent to the
     code that Brian quotes.

  3. The assert does not correspond to executable code, but is an assertion
     that the compiler can use as an assumption in compiling code (in Ada
     terms you can almost think of this as saying that the semantics of the
     assert is that the execution is erroneous if the condition is false).
     In this interpretation the *first* of the divide by zero checks in the
     above example can be omitted.

If this is not completely clear, that's not surprising, this is a messy
area to be absolutely sure of what the other guy is talking about :-)