[m-dev.] syntax for pre and post conditions

[Fergus Henderson]

On 24-Jan-2000, Peter Ross <petdr at cs.mu.OZ.AU> wrote:
> 
> I have been thinking about a syntax for pre and post conditions and
> think that using the syntax for post-conditions as suggested by Fergus
> is adequate
> 
> :- check Atom(Vars) => ExecutableFormula(Vars).

I don't think that syntax is adequate for *both* pre- and post-conditions.
That syntax works fine for post-conditions, but you need something
different for preconditions.
(Or alternatively, you could use that syntax for pre-conditions
and use a different syntax for post-conditions, but I think
it would be better to do it the other way around, since as
Peter Schachte explained that syntax doesn't seem right for
preconditions.)

> The pre conditions for a single mode of predicate can then be extracted
> by the following process, I believe.
> Create a new predicate with the following definition
> 
> new(Vars) :-
>     ExecutableFormula(Vars),
>     Atom(Vars).
> 
> Then run mode checking and see which parts of ExecutableFormula are
> possible to be left before the call to Atom, and hey presto you have
> your pre-condition.

That process is the right one to follow.  But I wouldn't describe
it as converting a post-condition into a pre-condition.
Instead I'd describe it as converting an admissibility constraint
into a pre-condition.  You could do something similar with post-conditions,
converting a success set constraint into a post-condition.

I should explain my terminology.
When dealing with specifications for logic programs,
you need to go to 3 (or more) valued logic:
a given ground goal can be true, it can false,
or it can be meaningless.
A ground goal is defined as _admissible_ if the intended interpretation
assigns it a definite truth value (i.e. true or false, not meaningless).
An _admissability constraint_ (e.g. `admissible(P) => Q')
specifies some bounds on the set of admissible goals.
The _admissible set_ for a predicate is the set of ground calls
to that predicate which are admissible.
Admissibility is a meta-logical notion (since it steps outside the
usual two-valued logic).  But it is a declarative notion;
it relates to the declarative specification, not to the operational
behaviour.

Similarly, the _success set_ for a predicate is the set of
ground goals which are true.  A success set constraint
(e.g. `P => Q') specifies some bounds on the success set.
This is also a declarative notion.

Pre-conditions and post-conditions are the operational notions
that corresponds to the declarative notions of admissible set
and success set (respectively).  While admissibility and the
success set relates to predicates and ground goals, pre-conditions
and post-conditions relate to procedures, i.e. specific modes of
predicates.

You can determine pre-conditions from admissibility constraints
or post-conditions from success set constraints in exactly
the manner that you describe above: essentially, the precondition
is the part of the admissibility constraint which applies to
the arguments or parts thereof which are bound on entry to the
procedure, while the postcondition is the part of the success
set constraint which applies to the arguments or parts thereof
which are bound when the procedure succeeds (which will typically
be all of it, since normally all the arguments will be ground
on exit, but that is not necessarily the case).

> For example the predicate zip(A,B,C) is true iff the list C is the pairs
> made up from lists A and B, where the lists A and B must have the same
> length.
> 
> :- check zip(A,B,C) => (length(A) = length(B), length(A) = length(C)).
> 
> :- pred zip(list(T), list(T), list(T)).
> 
> :- mode zip(in, in, out) is semidet.
> :- mode zip(out, out, in) is semidet.
> 
> zip([], [], []).
> zip([X|Xs], [Y|Ys], [X-Y|Zs]) :-
>     zip(Xs, Ys, Zs).
> 
> applying the above algorithm would leave us with 'length(A) = length(B)'
> as the pre condition for the mode (in, in, out) and nothing as the pre
> condition for the mode (out, out, in).
> 
> Counter examples anyone?

The above example is a counter example.  The precondition for zip/3
should be empty.  It's not an _error_ to call zip/3 with lists of
different lengths, it just fails.  Well, at least that's what I might
very reasonably have intended when I wrote zip/3.  Perhaps you intended
something else, but documenting the success set constraint (and hence
the postcondition) is not sufficient, you also need to document the
admissibility constraint (and hence the precondition).  For your
intended semantics of zip/3, you would need to add an admissibility
constraint

	:- check admissable zip(A,B,C) =>
		(length(A) = length(B), length(A) = length(C)).

whereas for my intended semantics of zip/3 there would be no
admissibility constraint (other than the type declaration,
which can be regarded as a statically checked form of admissibility
constraint).


Is all that clear?

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