[m-dev.] On the addition of assertions

[Peter Ross]

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.

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