[m-dev.] for review: document assertions.

[Fergus Henderson]

On 16-Jul-1999, Peter Ross <petdr at cs.mu.OZ.AU> wrote:
> doc/reference_manual.texi:
>     Document that usage of assertions.

s/that/the/

Overall, I think that documentation needs quite a bit of work.
Sorry for the slow review.

...
> +* Assertions::        Assertion declarations allow you to declare laws
> +                      that hold.

That should be changed to refer to `promises' rather than `assertions'.

I don't think "allow you to declare laws that hold" is a good summary.
After all, it's also possible to declare laws that don't hold.
And it's not really clear what they would be useful for.

> + at node Assertions
> + at chapter Assertions
> +
> +Mercury supports the declaration of laws that hold for predicates and
> +functions.  

See comments above.

> +These laws are only checked for type-correctness,
> +it is the responsibility of the programmer to ensure overall correctness.
> +The behaviour of programs with incorrect laws is undefined.

It's not clear what an "incorrect law" is, or what "overall correctness"
is, or what the programmer must do to achieve it.

> +A new law is introduced with the @samp{:- assertion} declaration.
> +
> +Here are some examples of @samp{:- assertion} declarations.
> +The following example declares the function @samp{+} to be commutative.
> +
> + at example
> +:- assertion
> +    all [A,B,R] (
> +        R = A + B
> +    <=>
> +        R = B + A
> +    ).
> + at end example

That's a bad example (or at least an insufficiently well explained
example); why not just write

	:- assertion all [A,B] (A + B = B + A).

?

> +Note that each variable in the declaration was explicitly quantified.
> +The current Mercury compiler requires that each assertion begins with
> +an @samp{all} quantification, and that every variable is explicitly
> +quantified.

I think the first part of the second sentence there is now false,
isn't it?

But my most important criticism is that this documentation fails
to make clear the purpose of these declarations.

See also Lee Naish's comments from July.

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