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

[bobduff@world.std.com (Robert A Duff)]

In article <dewar.835633172@schonberg>, Robert Dewar <dewar@cs.nyu.edu> wrote:
>Bob Duff said
>
>"
>    pragma Suppress(Assertion_Check);
>    pragma Assert(...);
>"

>Not quite, remember that failing an assertion raises Assert_Error, it is
>not erroneous, so the compiler cannot assume (not P) at the point where
>the assert appears, it can only assume (not P) after the asssertion
>which is a VERY much weaker condition.

What's "not P"?  Are you assuming the above is "pragma Assert(not P);"?

According to 11.5(26), failing a check IS erroneous, if that check has
been suppressed.  According to 11.5(27), an implementation may "add
additional check names, with implementation-defined semantics" -- such
as the Assertion_Check that I invented, above.

Since failing the suppressed check would be erroneous, this can affect
the generated code both before and after the assertion, depending on how
smart your optimizer is.  I'm not sure what you mean by "at the point
where the assert appears" -- it's been suppressed, and will therefore
presumably not generate any code.

Of course, if the assertion is not suppressed, then the compiler can
only know that the condition is true following the check.

Perhaps I'm misunderstanding what you said, but it seems to me that in
this regard (what the compiler can and cannot assume, with and without
pragma Suppress) the pragma Assert is just like a normal constraint
check (except, of course, that Asserts can have side-effects :-( ).  Of
course, pragma Assert is implementation defined, so it can have whatever
semantics the implementer wants.

- Bob