[m-dev.] On the addition of assertions

[Fergus Henderson]

On 24-Aug-1999, Peter Schachte <schachte at cs.mu.OZ.AU> wrote:
> On Tue, Aug 24, 1999 at 05:21:08PM +1000, Peter Ross wrote:
> > There are two reasons that I can think of why an assertion would be
> > needed in a different module
> >     * optimization purposes
> >     * proving properties of predicates
> 
> I think it's much better practice to put assertions in the same file
> as the predicate they're describing.  Otherwise if the source code is
> changed, it's very difficult to remember to change the assertion.

I think that in practice it is not quite as simple as that.
Often an assertion may be intended to describe one predicate (or function),
but it may mention several different predicates and/or functions.
Some of these may be from other modules.
For example, consider the following eminently reasonable code:

	:- module integer_utils.
	:- import_module integer.
	:- interface.

	% truncating integer square root on arbitrary precision integers
	:- 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.

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