[m-dev.] Assertion languages, optimisation & proof
fjh at cs.mu.OZ.AU
Fri Apr 24 03:41:33 AEST 1998
On 23-Apr-1998, David Glen JEFFERY <dgj at cs.mu.OZ.AU> wrote:
> The goals of introducing these assertion declarations seem to have become
> much broader.
> Some of the potential uses for these assertions that
> have cropped up in discussions are:
> - To allow the compiler to optimise certain programs where the
> optimisation relies upon a particular property. (eg. accumulator
> introduction, which relies on associativity)
> - for input and output assertions for predicates
> - for imposing invariants on types.
Those are examples of different *sorts* of assertions, not of different
*uses* for assertions. They just raise more questions ;-), e.g.
what are you going to do with these invariants on types?
> (BTW, wouldn't it be cool to make
> io__read fail if the term it read in didn't satisfy the invariants?)
Yes, I think that would be a very cool use of invariants :-)
All it needs is a new field in the type_info, a new function
`:- func type_invariant(type_info) = maybe(pred(T::in) is semidet)'
in std_util.m, and a tiny bit of SMOP to glue it all together.
[On another point, perhaps we should move the various type-related
procedures from std_util.m to a new module called say types.m.]
> My question concerns the last two (invariants on preds and types). If we
> only use these kinds of assertions for optimisation (eg. optimising away
> call to error/1), then there is no conceptual problem. However, if we are
> going to use this "meta-language" of assertions for proving properties of a
> program which potentially affect program correctness, we need to be more
> careful since we are changing the definition of static program correctness.
I think it would be a mistake to define static program correctness
in terms of assertions. We should leave the existing definitions
of type-correctness and determinism-correctness alone.
What I want to use assertions for is
- for programming by contract
Here assertions are mainly used as a formal form of documentation,
but programming by contract could be assisted by compiler options
to insert run-time checks of preconditions, postconditions,
- for formal verification
External theorem provers could use them to prove correctness
of the clauses for a predicate with respect to the specification.
- for declarative debugging
The theory at least is that assertions can be used to
reduce the number of questions asked by declarative debuggers.
Fergus Henderson <fjh at cs.mu.oz.au> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger fjh at 184.108.40.206 | -- the last words of T. S. Garp.
More information about the developers