[m-dev.] On the addition of assertions

[Peter Ross]

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

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

Accumulator introduction requires an assertion declaring that a
predicate is commutative.

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.

The problem with option b) is that inside an interface section :-
import_module only imports the types/modes and insts of a module.
This means that any predicate/function symbols used by the assertion
will not be recognised.

I think that the best approach would be a hybrid of the two and have
:- spec_interface and :- spec_implementation sections, where assertions
inside the spec_interface sections can be used in other modules.

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