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

[Peter Schachte]

On Mon, Jan 24, 2000 at 05:31:50PM +1100, Peter Ross wrote:
> Hi,
> 
> 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).
> 
> This gets around the problem of the pre and post conditions being
> dependent on which mode of the predicate is being called, by turning the
> pre condition into a post condition (it doesn't matter where the
> condition fails).
> 
> 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.

I assume this is just a sketch.  You don't want the predicate to fail
when its preconditions fail, you want an error message (like assert in
C).  That actually makes it all a lot messier.

>From your description, it sounds like anything that doesn't qualify as
a precondition would then be treated as a postcondition?  This sounds
good to me.  

You might want to use a term like "integrity constraint," which is
noncommittal about sequence, rather than "pre/post-condition."

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?


-- 
Peter Schachte                     If you think education is expensive, try
mailto:schachte at cs.mu.OZ.AU        ignorance.
http://www.cs.mu.oz.au/~schachte/      -- Derek Blok 
PGP: finger schachte at 128.250.37.3  
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------