[m-dev.] On the addition of assertions

[Fergus Henderson]

On 24-Aug-1999, Peter Ross <petdr at cs.mu.OZ.AU> 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
> 
> The only diffenence between these two options is what happens when an
> assertion needs to be used inside a different module.

Well, there are also differences as far as users are concerned.
For users option b) would probably be preferable.

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

This is a bad example.  If the programmer declares float:'+' to be commutative,
then they have lied to the compiler, and so they deserve to be punished ;-)

If we want to support that kind of thing, then it should be via
a separate pragma saying whether the compiler is or is not allowed to
rearrange floating point arithmetic, not via an assertion.
However, even then it would still be a bit problematic, since
such rearrangements could break referential transparency.

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

For proper uses of assertions, the assertion should be true universally,
not true in some modules and false in others.  So that's not an issue
for proper uses of assertions.

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

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.

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