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

[David Glen JEFFERY]

On 24-Apr-1998, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> > 	- 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?

Yes. You are right. However, we should probably consider both kinds at the
same time in order to make their syntaxes similar etc.

> [On another point, perhaps we should move the various type-related
> procedures from std_util.m to a new module called say types.m.]

Yes, that's a good idea.

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

Just a thought:

Perhaps we can look at using Lee's declarative (polymorphic) modes.
Using that system, you can certainly express more complicated things than our
current mode system. (eg.  these two lists contain the same elements, but
maybe in a different order.) It may well be worth looking at just how much you
can express in that system, and whether or not it meets our needs.

It would be a pity to get further down the track and realise that our 
input/output assertions are made redundant by a more expressive mode system.

Lee?

> What I want to use assertions for is
> 
> 	- for programming by contract
> 	  
> 	- for formal verification
> 
> 	- for declarative debugging

I suspect that no extension to the mode system alone will be sufficiently
expressive for all these things. (I would imagine that once the assertions
become sufficiently expressive, you will throw away things like decidability).

Also, there is one more thing that should be added to the list:
	
	- to aid the optimiser

As we've said, though, perhaps these should be a different form of assertion.


love and cuddles,
dgj
-- 
David Jeffery (dgj at cs.mu.oz.au) |  Marge: Did you just call everyone "chicken"?
MEngSc student,                 |  Homer: Noooo.  I swear on this Bible!
Department of Computer Science  |  Marge: That's not a Bible; that's a book of
University of Melbourne         |         carpet samples!
Australia                       |  Homer: Ooooh... Fuzzy.