[m-dev.] On the addition of assertions

Fergus Henderson fjh at cs.mu.OZ.AU
Wed Aug 25 17:47:26 AEST 1999

On 25-Aug-1999, Peter Ross <petdr at cs.mu.OZ.AU> wrote:
> On 24-Aug-1999, Zoltan Somogyi <zs at cs.mu.OZ.AU> wrote:
> > 
> > > How about the following alternative: assertion declarations are allowed
> > > in the interface, but the implementation never copies them to the `.int*'
> > > files, instead putting them only in the `.opt' and `.trans_opt' files.
> > > After type-checking the module, the implementation should check that any
> > > assertion declarations in the interface do not contain any symbols from
> > > modules imported only in the implementation.
> > 
> > That would work for the kinds of assertions Peter needs (e.g. associativity
> > for accumulator introduction). It would not work for assertions that state
> > "these two goals are mutually exclusive" (whatever specific term we end up
> > using for assertions of that type), because the determinism-correctness of
> > a module can depend on seeing assertions of this type that are made in other
> > modules.
> > 
> > However, I suppose we can worry about those kinds of assertions later.
> Those types of assertions would need to be distinguished anyway, so you
> could decide what to do depending on if you recognised the assertion as
> being of a special or not.

Yes.  For those kind of assertions, I think it would probablty be reasonable
to restrict them to only stating mutual exclusiveness about predicates
defined in that module.

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

More information about the developers mailing list