[m-dev.] On the addition of assertions

[Ralph Becket]

Fergus Henderson wrote on 24 Aug:
> 
> 	:- func integer_sqrt(integer) = integer.
> 	:- pragma assertion (
> 		all [X] (X >= integer(0) =>
> 			integer_sqrt(X) * integer_sqrt(X) =< X)
> 	).
> 
> Although this assertion is primarily about integer_utils:integer_sqrt/1,
> it also makes use of the functions integer:integer/1 and integer:'*'/2 and
> the predicate integer:'=<'/2.

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.

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?

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.)

Ralph

-- 
Ralph Becket  |  rwab1 at cam.sri.com  |  http://www.cam.sri.com/people/becket.html
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------