[m-dev.] On the addition of assertions

[Fergus Henderson]

On 24-Aug-1999, Ralph Becket <rwab1 at cam.sri.com> wrote:
> 
> It seems to me that assertions fulfill two purposes:
> 1. to provide suitably smart compilers with greater scope for
> optimisation (and, maybe, consistency checking); and
> 2. to provide helpful documentation to the code user.

Yes, there are lots of different purposes.
We've had a number of discussions about this in the past.
See my message "assertions summary" from last month for a
summary of the different kinds of assertions that
we might want, and proposal for names and syntax for them.

> The trouble is that code written for a smart compiler may not be
> accepted by a dumber compiler (e.g. if it can't prove various
> determinism declarations).  I'm not sure how much of a problem this
> is, especially given that determinism checking is undecidable in the
> worst case and that therefore the same situation arises.  What's the
> official line on this?

The official line is that compilers are not allowed to take assertions
into account when determining whether or not programs are legal.
In other words, they are required to use the standard algorithm for
determinism analysis.  

Compilers can of course use smart algorithms for optimization.
These algorithms can rely on information in "promise" assertions
(which are the only kind that the current ROTD supports).
But they must not rely on information in "contract" assertions.

Compilers can however perform consistency checking of "contract"
assertions, and they can use smart algorithms when doing such checking.

> On the other hand, I may have this wrong: assertions are not merely
> optimisation hints, but support qualititatively different coding
> styles.  If this is the case then they shouldn't be pragmas since, as
> I understand it, a program should be just as valid with all the
> pragmas stripped out (modulo C stuff etc.)

Right.  If we want to take certain kinds of assertions into account
for purposes of determinism analysis, then we should add special syntax
for those assertions.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------