[mercury-users] Library v2 and Typeclasses'n'Stuff

[Fergus Henderson]

On 30-Oct-1999, Michael Day <mikeday at corplink.com.au> wrote:
> 
> > - make extensive use of assertions/promises.
> 
> What exactly are assertions/promises?

This question has been discussed in great detail on the
mercury-developers mailing list.  See
<http://www.cs.mu.oz.au/mercury/mailing-lists/mercury-developers/mercury-developers.9907/0225.html>
for a summary.

But in brief, a "promise" is a statement by the programmer
that a given logical formula is true.  Unlike an ordinary
clause, a promise can have an arbitrary form: it need not
be in horn clause form and it need not be mode correct.
The compiler is allowed, but not required, to take promises
into account when computing answers.  So the compiler
can use promises for optimization, or it can ignore them.

Currently the development version of the compiler allows the
syntax `:- assertion' for promises.  But that will soon change
to `:- promise'.  As yet they are not documented in the
language reference manual.

> The one assertion I've stumbled
> across was in the int module,
> 
> :- assertion all [A,B,C] ( C = B * A <=> C = A * B ).
> 
> does the compiler take advantage of this somehow when optimising,

Yes, the compiler does take advantage of this when optimizing.
In particular, the `--introduce-accumulators' option

|	--introduce-accumulators
|      		Attempt to introduce accumulating variables into
|		procedures, so as to make them tail recursive.

needs information about which procedures are associative and
commutative in order to be able to transform non-tail-recursive
procedures into tail-recursive procedures using an accumulator-passing
style.  For some examples, see the files in tests/general/accumulator
in recent release-of-the-day release of the Mercury test suite, which
is available from our ftp site at
<ftp://ftp.mercury.cs.mu.oz.au/pub/mercury/beta-releases/>.

> Would more widespread use of
> assertions improve the quality of the code, or the readability of the
> code, or both?

In general, widespread use of "promise" declarations would probably
not improve anything except efficiency, and even then only in rather
specific cases.

There are other kinds of statements or assertions that programmers
might want to make about their code, in particular admissability
constraints (i.e. preconditions), success set constraints (i.e.
postconditions), specifications, and such like.  Some of these may
be checkable at runtime, others may not be feasible to check at all,
except perhaps via theorem-proving methods.  We think it would be a
nice idea to extend Mercury syntax to allow such things, and to
develop tools for helping programmers use formal methods to help
prove properties about their programs.

-- 
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-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------