[m-dev.] On the addition of assertions

[Peter Schachte]

On Tue, Aug 24, 1999 at 05:21:08PM +1000, Peter Ross wrote:
> This email is about where assertions should be placed in a Mercury
> source file.
> 
> There is two options
>     a) have a seperate assertions/specification section
>     b) have pragma style assertions that reside in the
>        interface/implementation sections

I prefer option b because:

     o	it's simpler
     o	it's a smaller change to the language
     o	it's more flexible for users
     o	it encourages (or at least doesn't discourage) putting such
	statements where they usually belong:  close to the predicates
	being described.

> The only diffenence between these two options is what happens when an
> assertion needs to be used inside a different module.
> 
> 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.
Also, there's no hope of automatically checking the validity of an
assertion in another module.  It's kind of like putting the
implementation for a predicate in one module, and putting its
interface in the modules that want to call it.

I recognize that it may be desirable to be able to make assertions
about predicates in other modules.  You may not have the source for a
predicate whose properties you may want to promise, and sometimes you
will want to describe a relationship between predicates in different
modules.  Still, the problems with allowing this seem worrisome enough
to me that it's not clear that it should be allowed.

> Now imagine a situation where a programmer has declared float:'+' to be
> commutative, intending it to mean float:'+' can be considered
> commutative for the current module so accumulator introducation can be
> used.
> 
> Option a) has no controls on the visibility of the assertions, so the 
> assertion may escape out to any module that imports the current module,
> where the programmer didn't intend float:'+' to be considered to be
> commutative.

I don't get it.  Either it's commutative or it's not.

Maybe you'd like to be able to say that for the purposes of a
particular predicate that calls +, it is commutative.  But saying it
for a whole module, and not for other modules, seems strange.
Occasionally useful, but also dangerous (it's too easy to add a new
call to + to that module and have it go wrong because + isn't
commutative for that call).

It would be better, I think, to invent some kind of qualified
commutativity: it's commutative as long as the arguments have a
certain property, and then declare that the arguments of some
predicates have that property.


-- 
Peter Schachte                     We don't know who discovered water, but
mailto:schachte at cs.mu.OZ.AU        we are certain it wasn't a fish.
http://www.cs.mu.oz.au/~schachte/      -- John Culkin 
PGP: finger schachte at 128.250.37.3  
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------