[m-dev.] Assertion languages, optimisation & proof

[Fergus Henderson]

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)

Yep.

> 	- 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,
	  and/or invariants.

	- 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 128.250.37.3        |     -- the last words of T. S. Garp.