[mercury-users] Pre- and Post- conditions

[Peter Schachte]

On Wed, Oct 07, 1998 at 04:47:56PM +1000, Patrick KREPS wrote:
> 
> I'm working on the development of pre- and post- conditions for Mercury.
> For memory, pre- and post- conditions of a certain procedure can be used
> to test conditions on the input and output arguments.

I don't think pre- and post- conditions are quite the right concept
for a relational language like Mercury, because predicates may have
multiple modes.  I think it's better to think in terms of which
predicate is at fault when the test fails: for "preconditions," the
fault lies with the caller, while for "postconditions," it is the
predicate itself that is at fault.  I find it better to think of these
as integrety constraints and admissibility conditions.  These
correspond roughly to postconditions and preconditions, respectively.

Here's an example of an integrity constraint (making up a syntax):

	:- promise sort(_, L) => sorted(L).

(The idea here is that there should be a single goal with all
arguments distinct variables before the arrow; this indicates which
predicate is being described.)

This would say that whenever sort/2 succeeds, the resulting list is
sorted.  Logically, it says that

	\forall x (sort(x, l) \implies sorted(l))

which is the same as

	(\exists x : sort(x, l)) \implies sorted(l)

so the "variables are existentially quantified in their closest
enclosing scope" rule for the :- promise form above would give the
right reading.

A more interesting example would be:

	:- promise map_search(Map, Key, _) <=> map_contains(Map, Key).

This says that whenever map_lookup(Map, Key, Value) succeeds for some
Value, then Map contains the key Key.  It also says that whenever Map
contains Key, then there is a Value such that map_lookup(Map, Key,
Value) succeeds.  Thus you are providing useful information about
map_search/3, whether is succeeds or fails.  You might also want to
say

	:- promise map_search(Map, _, _) <=> \+ map_empty(Map).

These can all be viewed not just as conditions to test to check up on
an implementation of a predicate, but also as hints to the compiler
that may allow it to optimize code.  For this reason you may want to
have another keyword like

	:- ensure map_search(Map, Key, _) <= map_contains(Map, Key).

which would have the same semantics as a `promise' directive, but
would tell the compiler that when some debugging flag is specified the
code for map_search/3 should be enhanced so that when map_search(Map,
Key, _) fails, the code checks that map_contains(Map, Key) also fails;
if not, it signals an error.

Admissibility constraints are a bit different.  They allow you to
specify when a predicate makes sense.  I believe this is Lee Naish's
idea, so I'll phrase it the way he would: they let you specify which
part of the success set of a predicate is the intended interpretation.
Take, for example:

	:- pred merge(list(T), list(T), list(T)) <= partial_order(T).

	merge([], L, L).
	merge(L, [], L).
	merge([A|As], [B|Bs], [C|Cs]) :-
		(   A =< B ->
			C = A,
			merge(As, [B|Bs], Cs)
		;   C = B,
		    merge([A|As], Bs, Cs)
		).

This predicate merges two sorted lists to produce a sorted list.  It
could also partition a sorted list into all possible pairs of sorted
lists if Mercury were a little more logical about if-then-elses.
Unfortunately, it doesn't seem to be possible to write a reversible
merge predicate that gets the determinism right in Mercury.  If it
were, other combinations of modes would be useful, too.  But anyway,
this predicate doesn't do anything very useful when the inputs,
whichever argumentst they are, aren't sorted.  So I might want to
declare

	:- admissible merge(As, Bs, Cs) <= sorted(As), sorted(Bs),
					   sorted(Cs).

This would state that whichever of As, Bs, and Cs are ground when
merge(As, Bs, Cs) is called, they should be sorted, and this should be
tested when the code is compiled in debug mode.  If the admissiblity
constraint is not satisfied, an error should be reported, because the
predicate is being applied outside its intended interpretation, so its
results will be meaningless.  This declaration probably doesn't convey
any useful information to the compiler, though, because it's not
describing what is outside vs. inside the success set, only what is
outside vs. inside the intended interpretation.

The difficult question is what to do about tests involving arguments
that are not ground on input.  The idea of these tests, and of the
`promise' and `ensure' conditions mentioned above, is that the they
should be semidet with no outputs, so the tests should not be
performed until all the arguments are sufficiently bound.  But should
they be performed once the arguments /are/ sufficiently bound?  Doing
this actually tests that the predicate produces only solutions that
are in the intended interpretation of the predicate.  My feeling is
that these tests should probably be done, but there may be good
examples where it would interfere.  In any case, if these later tests
are performed and they fail, the error message must ascribe blame to
the predicate itself, rather than the caller.


-- 
Peter Schachte                | I disapprove of what you say, but I will
mailto:pets at cs.mu.OZ.AU       | defend to the death your right to say it.
http://www.cs.mu.oz.au/~pets/ |     -- Voltaire 
PGP: finger pets at 128.250.37.3 |