[m-dev.] On the addition of assertions

Peter Ross petdr at cs.mu.OZ.AU
Wed Aug 25 15:26:32 AEST 1999

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.

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

More information about the developers mailing list