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

[Peter Ross]

On 24-Jan-2000, Peter Schachte <schachte at cs.mu.OZ.AU> wrote:
> 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.
> 

Yes, once you have identified the pre and post conditions, you generate
code like

atom(Vars) :-
    (
        pre-condition(Vars)
    ->
        Atom(Vars),
        (
            post-condition(Vars)
        ->
            true
        ;
            throw(post)
        )
    ;
        throw(pre)
    ).

I assume that the declarative debugger could catch the exceptions and do
the correct thing.


> >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?
> 
You are correct, the implication is pointing the wrong way (not Fergus's
fault, but mine).  However in a sense it is not an admissibility check,
as admissibility is only concerned with what values are valid input, and
ExecutableFormula may only check the success set.  However something
like your second suggestion may be better, so that people don't get the
implication the wrong way around (as if anyone would be that stupid ;) ).

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