[mercury-users] Pre- and Post- conditions

[Lee Naish]

<Peter kindly forwarded his posting to me; I'm not actually subscribed to
this mailing list>

   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,

I also find work on pre- and post- conditions in LP tends to be more
procedural and less declarative than it could be (I can't comment on
Patrick's proposal).

   Admissibility constraints are a bit different.  They allow you to
   specify when a predicate makes sense.  I believe this is Lee Naish's

I have used the term "type" in a very general way for this.  I have also
used "admissibility" in the context of debugging (after Pereira) and
semantics (grep for three-valued in my papers).  The most obvious
definition of admissibility is well-typed.  However, it turns out to be
more natural to associate admissibility with well-typedness of just the
input arguments.  In mercury you could probably get away with just one kind
of declaration giving properties of the intended interpretation of a
predicate, then use the modes to separate out the pre-/admissibility
conditions from the post-/correctness conditions.  However, having separate
declaration is probably easier for the users.  One possibility to get
around the problem of pre-/admissibility conditions with multiple modes is
to add these conditions to mode declarations in some way (eg, an optional
"where condition_on_inputs").  The intended meaning should be a subset of
the the predicate definition along with all the declarations.

One general point about assertion languages - I think its helpful to look
at declarative debugging to show what kind of assertions are important. One
kind of assertion typically allows you to identify incorrect answers (that
tends to be done reasonably well in most proposals).  However, there is
another aspect which is identifying missing answers.  This is rather more
subtle and most proposals have not done a good job (even those specifically
designed for declarative debugging).  An exception (in my opinion) is the
language for assertions I designed for the NU-Prolog debugging environment
(NUDE).  Unfortunately its not been written up (I should do it one of these
days) and I keep prodding Bert to finalise the cleaning up the
implementation for the release of the system <prod> <prod>.

Another thing to look at is work by Manuel Hermenegildo et al on the
assertion language used in the CIAO system (herme at clip.dia.fi.upm.es can
give you more details).

     lee