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

[kst@thomsoft.com (Keith Thompson)]

[Newsgroups trimmed to comp.lang.ada]

In <dewar.835306677@schonberg> dewar@cs.nyu.edu (Robert Dewar) writes:
> In GNAT, 
> 
>    pragma Assert (X);
> 
> means EXACTLY
> 
>    if not X then
>       raise Assert_Error;

System.Assertions.Assert_Failure, actually.

>    end if;
> 
> which is well defined, but not at all in the category of assertions that
> the compiler can take advantage of, which can behave in a completely
> differrent (and possibly suprising manner).

I'm not sure I understand your point here.  For example:

   declare
      X: Integer := Some_Unknown_Value;
      Y: Integer := Another_Unknown_Value;
      Z: Integer;
   begin
      pragma Assert(X /= 0);
      Z := X / Y;               -- What may be assumed here?
      Put_Line("Z = " & Integer'Image(Z));
   end;

If the pragma Assert is equivalent to the if statement shown above,
then surely the compiler can assume that X /= 0, and can eliminate the
divide-by-zero check, if assertion checking is enabled.  After all,
if X is zero the division will never be executed.  (Note that X is not
volatile, shared, aliased, or anything fancy like that).  Whether the
current version of GNAT actually does this is another question.

What gets interesting is having an option to disable assertion checking
(as GNAT does).  If the checking is disabled, may the compiler still
assume that X /= 0?  GNAT has chosen not to make this assumption.
The alternative model (which I prefer) is to treat assertions in much
the same was as predefined checks; execution of code that violates an
assertion is erroneous.

Personally, I wish the assert statement of Preliminary Ada (the 1979
version) had remained in the language, preferably with an extension to
allow it in declarative parts.  Assertion checking could be disabled with
"pragma Suppress(Asssert_Error);".

By the way, here's another way to implement assertions without special
compiler support:

   declare
      subtype Truth is Boolean range True .. True;
      X: Integer := Some_Unknown_Value;
      X_Non_Zero: constant Truth := X /= 0;
      Y: Integer := Another_Unknown_Value;
      Z: Integer;
   begin
      Z := X / Y;
      Put_Line("Z = " & Integer'Image(Z));
   end;

The declaration of Non_Zero raises Constraint_Error if the assertion
fails, and will probably trigger a compiler warning if it fails
statically.  This is probably an incomplete solution, since I *think* the
compiler is allowed to eliminate X_Non_Zero if it's never referenced.
Perhaps pragma Volatile can be used to work around this, but that
introduces other complications.

-- 
Keith Thompson (The_Other_Keith) kst@thomsoft.com <*>
TeleSoft^H^H^H^H^H^H^H^H Alsys^H^H^H^H^H Thomson Software Products
10251 Vista Sorrento Parkway, Suite 300, San Diego, CA, USA, 92121-2718
"As the most participatory form of mass speech yet developed, the Internet
deserves the highest protection from government intrusion." -- ACLU v. Reno