[m-dev.] Declarative debugger and pre and post conditions

[Ian MacLarty]

Originally my idea was to be able to write compilable specifications 
which would just be a version of the predicate with the modes of all 
the arguments being `in'.  To satisfy its specification a predicate 
should be logically equivalent to its specification.  For example the 
spec for a sort predicate might look like:

sort_spec(A, B) :- list.perm(A, B), ordered(B).

where ordered/1 just checked that the elements were in order.  Having 
all the arguments being input gives us maximum expressive power when 
writing the specification.

However these types of specifications do not in general help the 
declarative degubber work out if an invalid call is inadmissible (a 
pre-condition is violated) or erroneous (a post-condition is violated). 
  This information is important to the declarative debugger because it 
tells it in which part of the call tree the bug might be.  In fact the 
specification mechanism I've mentioned above wouldn't even cover the 
concept of inadmissibility.  A call would either be correct or 
incorrect and if it was incorrect there'd be no way in general to work 
out if it was the inputs that made the call incorrect and thus 
inadmissible.

There are also similar problems with the weaker "requirements" 
suggestion.  For example suppose we had the following requirements on a 
predicate p:

:- pragma ensure(p(A, B), (A < B, B =< 10)).

Now suppose the call p(10, 11) succeeded where 10 was input and 11 was 
output.  Clearly the requirements have been violated, but if we use the 
suggested method of assuming that requirements that mention only inputs 
are preconditions and requirements that mention outputs are 
postconditions, then we'd infer that a postcondition was violated 
(since the requirement B =< 10 was violated).  However if we intended p 
not to be called with it's first argument >= 10, then a precondition 
has been violated.  We could explicitly add this as a requirment : (A < 
B, B =< 10, A < 10), but this seems redundant as it's already implied 
by the existing requirments.

I think it's important to seperate out pre and post conditions so it's 
plain whether these are conditions the caller or the callee should 
fulfil.  A specification mechanism needs to seperate these two concepts 
out so the declarative debugger can work out if it's the caller or the 
callee that's not doing the right thing.

I therefore support the idea of each mode of a predicate having it's 
own set of preconditions.  Each precondition would be a statement about 
the `in' arguments in that mode.  This makes it clear that this is an 
extra condition we require the caller to adhere to when calling the 
predicate in that mode.  This also reflects the reason for needing a 
preconditon in the first place : the implementation of the predicate is 
only designed to work for calls who's inputs satisfy a certain 
condition, which is similar to the reason we have mode declarations - 
with a mode declaration we are saying the implementation of the 
predicate is only designed to work when certain arguments are ground.

This may lead to preconditions for different modes contradicting each 
other, but I don't see that as a problem in real applications as most 
predicates tend to only have one mode anyway.  Also modes could be 
grouped together under one precondition as long as the arguments in the 
preconditon are `in' for all the modes the precondition applies to.

Post conditions wouldn't need to be mode specific and could be 
expressed much like the specification mechanism shown before, except 
they would only apply when the call succeeded, so they wouldn't be 
logically equivalent to the predicate - they would just be implied by 
the predicate.

I don't see this mechanism being used as a runtime assertion checking 
mechanism that would throw an exception when a call doesn't satisfy 
it's pre or post conditions.  I don't think a specification mechanism 
should change the semantics of the program it's specifying.  Instead 
the program could be compiled with a --check-conditions flag and the 
generated executable would run normally, but would produce a report 
afterwards saying which calls violated their pre and post conditions.  
Runtime assertion checking that throws an exception can be done with 
require.require/2.

Ian.

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