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

[Fergus Henderson]

On 25-Jan-2000, Peter Ross <petdr at cs.mu.OZ.AU> wrote:
> On 24-Jan-2000, Peter Schachte <schachte at cs.mu.OZ.AU> wrote:
> > The semantics of Fergus's notation seems a bit off, though.  To me,
> > the natural reading is something like "for all Vars, Mercury should
> > check whether Atom(Vars) implies ExecutableFormula(Vars)," which isn't
> > what is intended.  What you really want to say is that Atom(Vars) is
> > only guaranteed to behave properly when ExecutableFormula(Vars) holds,
> > an furthermore, the user would like the Mercury system to check that
> > whenever Atom(Vars) is invoked, ExecutableFormula(Vars) holds, and
> > holler if it doesn't.  At the very least the implication seems to be
> > pointing the wrong way: you're saying that ExecutableFormula(Vars)
> > implies that Atom(Vars) make sense (is admissible).  Maybe something
> > like
> > 
> > 	:- admissible Atom(Vars) <= ExecutableFormula(Vars).
> > 
> > or
> > 
> > 	:- when Atom(Vars) check ExecutableFormula(Vars).
> > 
> > would be clearer?
>
> You are correct, the implication is pointing the wrong way (not Fergus's
> fault, but mine).

No, the implication in the earlier example was in the correct
direction; the example immediately above has the direction wrong.
The reason is that what you're really saying is that if
ExecutableFormula is not true, then Atom is not admissible,
i.e.
	not(ExecutableFormula) => not(admissible(Atom))

which is equivalent to

	admissable(Atom) => ExecutableFormula

not to

	admissable(Atom) <= ExecutableFormula

Note that if ExecutableFormula is true, it does not guarantee that Atom
is admissable; there might be some additional admissibility constraints
that are not executable or that are simply not easy to express.

> However something
> like your second suggestion may be better, so that people don't get the
> implication the wrong way around

Indeed ;-)

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