[m-dev.] On the addition of assertions

[Zoltan Somogyi]

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

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