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

[Peter Moulder]

Should `ensure' raise an exception in the case that the predicate
ultimately fails?  E.g. if list__merge is called with all input
arguments, where the first two are sorted but not the third, then
should list__merge silently indicate `false' as in its current
implementation, or should it raise an exception as it would with the
proposal in the preceding message?

As Mercury is a logical language, many of the predicates in the standard
library are documented in terms of `iff', inviting use as a testing
predicate rather than as an operation producing output.  For the routine
`set__insert(Set0, X, Set)', it may be tempting to declare `ensure(not
empty(Set))' (which would indeed be a reasonable postcondition for the
normal in,in,out mode), but adding such a declaration would reduce the
usefulness of that predicate when passing Set as input.

When I was last thinking about how to adapt the notions of pre- and
postconditions to the Mercury language, it was in the context of
interfacing with proof-checking software.  The following notions are
logically rich, but need thought as to how to adapt them to simple
runtime checking.

The notion of postcondition can be subsumed by statements about a
predicate, such as

  all[Set0, X, Set] ( not set__insert(Set0, X, Set) ; not empty(Set) )

corresponding to saying that if set__insert succeeds then Set is
non-empty.

(That's not a suggested syntax, just an example of the sort of logical
statement about a predicate that one might wish to guarantee for
callers, and consequently that one might wish to put to the test, at
least for (Set0,X,Set) instances that have actually occurred at runtime.)


Preconditions are actually more complex to handle well for a declarative
language.  There's more than one type of precondition:

  - Operational preconditions, typically for foreign code.  E.g. for
    array__unsafe_set(OldArray, Ix, Elem, NewArray), one really does
    want Ix to be in bounds before executing the foreign code, it's not
    enough for the call to be in a conjunction with false or in a
    disjunction with true.  E.g. it's a bug to write

      array__semidet_set(OldArray, Ix, Elem, NewArray):-
      	array__in_bounds(OldArray, Ix),
	array__unsafe_set(OldArray, Ix, Elem, NewArray)

    as the compiler is free to reorder or interleave those conjuncts (in
    the default commutative semantics).

    One can distinguish two variants of operational preconditions,
    according to whether or not the precondition is considered to have
    failed in the above example if the current compiler implementation
    chooses to execute the two conjuncts in the order given: i.e.
    whether it is safe in the current run vs whether it is guaranteed to
    be safe for all allowed implementations.

  - Declarative preconditions, similar to one notion of the domain of a
    function.  The declarative semantics of a predicate `q(X):- r(X).'
    having declarative precondition p(X) would be

      all[X] ( not p(X) ; ( q(X) <=> r(X) ) ).

    I.e. nothing is known about the truth of q(X) for values of X where
    not p(X), much like the declarative semantics of erroneous
    predicates like `loop:- loop.'.  Here the `must be sound'
    requirement of Mercury implementations comes into play:

      Mercury implementations must be sound: the answers they compute
      must be true in every model of the theory.  Mercury
      implementations are not required to be complete: they may [abort].

    In particular, the program must abort rather than let execution
    depend on the truth of q(X) for values of X s.t. not p(X).

    Implementations are allowed (but not required) to offer fairly strong
    completeness guarantees such as using three-valued logic to reduce
    the occurrence of aborting when not required to by the `must be
    sound' requirement.

    Of course a more typical implementation would be to abort as soon as
    a call to q is encountered where not p(X).  This would then coincide
    with the `current call only' variant of operational preconditions.


Some of the above adaptations of the notions of pre- and postcondition
may be deemed unsuitable for implementation as simple runtime checks,
but I hope people give thought to declarative semantics and purity when
considering what to provide.  It would be nice if the facility assists
reasoning about programs rather than making it more difficult.

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