[m-dev.] On the addition of assertions

[Peter Ross]

On 24-Aug-1999, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> 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.
> 

Agreed.  However it is possible using the first of these proposals for
assertions to be used inappropiately and for them, arguably, not to do
what the programmer expected.

That IMHO is a problem.

> > 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.
> 
Sounds like a good idea.

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