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

[Zoltan Somogyi]

On 04-Oct-2004, Peter Schachte <schachte at cs.mu.OZ.AU> wrote:
> OK, I take your point:  there *are* two different kinds of
> "requirements."  But I still don't think they need to be specified per
> mode.

They *should* be specified per mode, because the obligations we impose
on the caller depend on the mode.

> but it seems wrong for the predicate to place
> expectations on its callers that it does not place on itself.

This objection can be answered by conjoining the preconditions of all
the modes together with any explicitly stated postcondition, which Ian was
planning on anyway for the long term. However, we agreed that doing this
was probably counterproductive (the cost in runtime outweighing any
theoretical or practical benefits) until we can optimize away the extra
checks using program analysis.

> I would argue that if q(X) is ever called with X bound to a value that
> does not satisfy p(X), then the program should abort.  My rationale is
> that even if some clever scheduling can let q(X) fail without
> aborting, the programmer is better off knowing that q/1 can be called
> with an unexpected input, rather than proceding in ignorance.

I agree.

> though once the execution has had some
> arguments not meet requirements, the behavior of the whole program is
> suspect.  So any error reports after the first may well have been
> caused by the first, just like C compiler error messages.  More
> importantly, if the program actually *does* something, like deleting
> files, you probably don't want to continue when you know something is
> wrong.  So I do think it's better to just abort when requirements are
> not satisfied.

I agree.

> In fact, I'd like to take expect and ensure declarations to suggest to
> the compiler that it try some compile-time theorem proving to minimize
> the number of runtime tests, and to report at compile time when
> requirements are sure not to be satisfied.  Perhaps with a certain
> switch, it should even report any requirements that cannot be proved
> at compile-time.

That's for next year at the earliest.

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