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

[Peter Ross]

Hi,

This still needs to be reviewed.

===================================================================


Estimated hours taken: 2

doc/reference_manual.texi:
    Document that usage of assertions.
    
doc/transition_guide.texi:
    Add assertion to the op table.


Index: reference_manual.texi
===================================================================
RCS file: /home/staff/zs/imp/mercury/doc/reference_manual.texi,v
retrieving revision 1.147
diff -u -r1.147 reference_manual.texi
--- reference_manual.texi	1999/07/15 06:25:06	1.147
+++ reference_manual.texi	1999/07/15 06:44:31
@@ -49,6 +49,7 @@
 @author Peter Schachte
 @author Simon Taylor
 @author Chris Speirs
+ at author Peter Ross
 @page
 @vskip 0pt plus 1filll
 Copyright @copyright{} 1995-1999 The University of Melbourne.
@@ -82,6 +83,8 @@
                       safely use destructive update to modify that value
 * Determinism::       Determinism declarations let you specify that a predicate
                       should never fail or should never succeed more than once
+* Assertions::        Assertion declarations allow you to declare laws
+                      that hold.
 * Equality preds::    User-defined types can have user-defined equality
                       predicates.
 * Higher-order::      Mercury supports higher-order predicates and functions,
@@ -358,6 +361,7 @@
 :- typeclass
 :- instance
 :- pragma
+:- assertion
 :- module
 :- interface
 :- implementation
@@ -2121,6 +2125,46 @@
 And there are a variety of other applications.
 
 @c XXX fix semantics for I/O + committed choice + mode inference 
+
+ at node Assertions
+ at chapter Assertions
+
+Mercury supports the declaration of laws that hold for predicates and
+functions.  
+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.
+
+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
+
+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.
+
+Here is a more complicated declaration. It declares that @samp{append} is
+associative.
+
+ at example
+:- assertion
+    all [A,B,C,ABC] (
+        (some [AB] (append(A, B, AB), append(AB, C, ABC)))
+    <=>
+        (some [BC] (append(B, C, BC), append(A, BC, ABC)))
+    ).
+ at end example
 
 @node Equality preds
 @chapter User-defined equality predicates
Index: transition_guide.texi
===================================================================
RCS file: /home/staff/zs/imp/mercury/doc/transition_guide.texi,v
retrieving revision 1.28
diff -u -r1.28 transition_guide.texi
--- transition_guide.texi	1999/07/13 08:54:37	1.28
+++ transition_guide.texi	1999/07/14 00:35:05
@@ -149,6 +149,7 @@
 aditi_top_down  fx              500
 all             fxy             950
 and             xfy             720
+assertion       fx              1199
 div             yfx             400
 else            xfy             1170
 end_module      fx              1199

----
 +----------------------------------------------------------------------+
 | Peter Ross      M Sci/Eng Melbourne Uni                              |
 | petdr at cs.mu.oz.au  WWW: www.cs.mu.oz.au/~petdr/ ph: +61 3 9344 9158  |
 +----------------------------------------------------------------------+
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------