[m-dev.] for review: document assertions

[Peter Ross]

Hi,

This is for Fergus to review.

Pete.


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


Estimated hours taken: 2


doc/reference_manual.texi:
    Add documentation of the assertion declaration.
    Fix some spelling mistakes.

Index: reference_manual.texi
===================================================================
RCS file: /home/staff/zs/imp/mercury/doc/reference_manual.texi,v
retrieving revision 1.140
diff -u -r1.140 reference_manual.texi
--- reference_manual.texi	1999/06/30 17:13:18	1.140
+++ reference_manual.texi	1999/07/08 02:40:38
@@ -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,13 +83,15 @@
                       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,
                       with closures, lambda expressions, and currying
 * Modules::           Modules allow you to divide a program into smaller parts
 * Type classes::      Constrained polymorphism
-* Existential types:: Support for data abstraction and heterogenous collections
+* Existential types:: Support for data abstraction and heterogeneous collections
 * Semantics::         Declarative and operational semantics of Mercury programs
 * Pragmas::           Various compiler directives, used for the C interface
                       and to control optimization.
@@ -349,6 +352,7 @@
 :- typeclass
 :- instance
 :- pragma
+:- assertion
 :- module
 :- interface
 :- implementation
@@ -762,7 +766,7 @@
 whose value is the predicate or function of the specified arguments
 determined by the specified goal.  @xref{Higher-order}.
 
-A lambda expression introduces a new scope: any variables occuring in
+A lambda expression introduces a new scope: any variables occurring in
 the arguments Arg1, Arg2, ... are locally quantified, i.e.
 any occurrences of variables with that name in the lambda
 expression are considered to name a different variable than any
@@ -2092,6 +2096,46 @@
 
 @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
 
@@ -2518,7 +2562,7 @@
 These insts represent the instantiation state of variables bound
 to higher-order predicate and function terms with the appropriate mode
 and determinism.
-For example, @samp{pred(out) is det} represents the instantion state
+For example, @samp{pred(out) is det} represents the instantiation state
 of being bound to a higher-order predicate term which is @samp{det}
 and accepts one output argument; the term @samp{sum([1,2,3])} from the
 example above is one such higher-order predicate term which matches
@@ -2980,7 +3024,7 @@
 parameters in the type class declaration.
 Each @samp{instance} declaration must define an implementation for
 every method declared in the corresponding @samp{typeclass} declaration.
-It is an error to define more than one implemention for the same
+It is an error to define more than one implementation for the same
 method within a single @samp{instance} declaration.
 
 Any call to a method must have argument types (and in the case of functions,
@@ -3109,7 +3153,7 @@
 @section Type class constraints on predicates and functions
 
 Mercury allows a type class constraint to appear as part of a predicate or
-functions's type signature.  This constrains the values that can be taken
+function's type signature.  This constrains the values that can be taken
 by type variables in the signature to belong to particular type classes.
 
 A type class constraint is of the form:
@@ -3277,7 +3321,7 @@
 % Here the type variables `T' is existentially quantified
 :- some [T] pred foo(T).
 
-% Here the type variabless `T1' and `T2' are existentially quantified.
+% Here the type variables `T1' and `T2' are existentially quantified.
 :- some [T1, T2] func bar(int, list(T1), set(T2)) = pair(T1, T2).
 
 % Here the type variable `T2' is existentially quantified,
@@ -3466,7 +3510,7 @@
 
 The standard library module @samp{std_util} provides a type
 named @samp{univ} which can hold values of any type. 
-You can form heterogenous containers (containers that can hold values of
+You can form heterogeneous containers (containers that can hold values of
 different types at the same time) by using data structures
 that contain @code{univ}s, e.g. @samp{list(univ)}.
 
@@ -3514,7 +3558,7 @@
 
 Unfortunately this technique doesn't work if you also want to use
 type class constraints.  Eventually we hope to support existentially
-typed data types with type class constaints, which would address this issue.
+typed data types with type class constraints, which would address this issue.
 @c (In the mean time, as a work-around, it is in fact possible to achieve
 @c the same effect via some hacks using the C interface.)
 
@@ -3596,7 +3640,7 @@
 semantics guarantees to compute an answer in finite time for
 any program for which an answer would be computed in finite time for all
 possible executions under the strict commutative semantics
-(i.e. for all possible orderings of conjuctions and disjunctions).
+(i.e. for all possible orderings of conjunctions and disjunctions).
 
 Thus, to summarize, there are in fact a variety of different operational
 semantics for Mercury.  In one of them, the strict sequential semantics, there
@@ -4539,7 +4583,7 @@
 Another use for the function trail is check for floundering
 in the presence of delayed goals.
 
-Often, when implementating certain kinds of constraint solvers, it may
+Often, when implementing certain kinds of constraint solvers, it may
 not be possible to actually solve all of the constraints at the time
 they are added.  Instead, it may be necessary to simply delay their
 execution until a later time, in the hope the constraints may become
@@ -4550,7 +4594,7 @@
 delayed goals which might cause failure, before execution commits
 to this execution path.  If there are any such delayed goals, the
 computation is said to ``flounder''.  If the check for floundering was
-omitted, then it could lead to unsound behavior,  such as a negation
+omitted, then it could lead to unsound behaviour,  such as a negation
 failing even though logically speaking it ought to have succeeded.
 
 The check for floundering can be implemented using the function trail,
@@ -4703,16 +4747,16 @@
 input/output) without taking an io__state (@pxref{Types}) as input and
 returning one as output, and do not make any changes to any data
 structure that will not be undone on backtracking (unless the data
-structure would be unreachable on backtracking).  The behavior of other
+structure would be unreachable on backtracking).  The behaviour of other
 predicates is never affected by the invocation of pure predicates, nor
-is the behavior of pure predicates ever affected by the invocation of
+is the behaviour of pure predicates ever affected by the invocation of
 other predicates.
 
 The vast majority of Mercury predicates are pure.  
 
 @item semipure
 Semipure predicates are just like pure predicates, except that their
-behavior may be affected by the invocation of impure predicates.  That
+behaviour may be affected by the invocation of impure predicates.  That
 is, they are sensitive to the state of the computation other than as
 reflected by their input arguments, though they do not affect the state
 themselves.
@@ -4796,7 +4840,7 @@
 with @code{impure} or @code{semipure}, compound goals never need this.
 See @ref{Impurity Example} for an example of this.
 
-The requiremment that impure or semipure calls be marked with
+The requirement that impure or semipure calls be marked with
 @code{impure} or @code{semipure} allows someone 
 reading the code to tell which goals are not pure, making code which
 relies on side effects somewhat less mysterious.  Furthermore, it means
@@ -4814,7 +4858,7 @@
 the procedural implementation from aggressive compiler optimizations.
 Of course, the Mercury compiler cannot verify that a predicate is pure,
 so it is the programmer's responsibility to ensure this.  If a predicate
-is promised pure and is not, the behavior of the program is undefined.
+is promised pure and is not, the behaviour of the program is undefined.
 
 The programmer may promise that a predicate is pure using the
 @code{promise_pure} pragma:
@@ -4941,7 +4985,7 @@
 
 Implementations are free to ignore @samp{pragma type_spec} declarations.
 Implementations are also free to perform type specialization
-even in the absense of any @samp{pragma type_spec} declarations.
+even in the absence of any @samp{pragma type_spec} declarations.
 
 @node When to use type specialization
 @subsection When to use type specialization
@@ -5097,7 +5141,7 @@
 
 In the current implementation, the table of facts is compiled into a
 separate C file named @samp{@var{FileName}.c}.  The compiler will
-automatically generate the correct depencencies for this file when the
+automatically generate the correct dependencies for this file when the
 command @samp{mmake @var{main_module}.depend} is invoked.  This ensures
 that the C file will be compiled to @samp{@var{FileName}.o} and then
 linked with the other object files when @samp{mmake @var{main_module}}
@@ -5171,7 +5215,7 @@
 true or false in the completion semantics is also true
 or false (respectively) in the minimal model semantics,
 but there are goals for which the minimal model specifies
-that the result is true or false, wheres the completion semantics
+that the result is true or false, whereas the completion semantics
 leaves the result unspecified. 
 For these goals, the usual Mercury semantics requires the
 implementation to either loop or report an error message,

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