Algebraic types and subclassing

[Andrew Butterfield]

At 11:47 pm +0000 12/3/98, Nick Kallen wrote:
>demand. Things like pre and post conditions, and the above "traits" or
>invariants are standard elements of Formal Method systems that I believe
>have had practical use in the defense industry.

The pre and post conditions are very much oriented to proving the
correcntess of imperative programs, and the same general ideas are useful
for functional programs. However, functional programs, because they compute
functions, without side-effects, don't require the full pre+post condition
machinery, which is designed for imperative languages with side effects
and partial hidden changes to implicit state.

> Extending
>Clean so that these specifications could be well integrated with the code
>would make the programmer's job that much easier.

On of the nice things about proving properties of functional programs is that
they can be expressed and  proved using functional notation - a lot of work
has been done in this area - so there is no need for a special specification
syntax - specs. can be written in Clean - they don't have to executable,
but if they are, then they can be called up at runitme to check various
conditions.

If they are not executable, then a theorem prover is needed,

>    A theorem prover that could reason through the traits, pre and post
>conditions, and prove that all of these things are satisfied (at compile
>time) is probably a long way off.

Interestingly, there is a nice theorem prover called PVS,
       http://www.csl.sri.com/pvs.html
which is very powerful, and uses a very functional style of higher order
logic. They state that theorems written in a functional style are much
easier to prove mechanically, than those written in existential style
(forall a exist y ...)

Another reason for keeping to a functional specification style.

Why do I say all this ? Because our research group has been working on
a functional variantt of VDM, called "Irish VDM", whihc essentially
recasts pre- + post conditions of VDM's logic of partial functions
into a more classical mathematical framework. We retain pre conditions
and invariants, but post-consitions are largely replaced by functional
descrptions of desired behaviour (OK, OK, you can call these post condition
computations, if you want).

We have some material on WWW - it needs tidying up - the Publications
link leads you to some material for reading

 http://www.cs.tcd.ie/research_groups/fmg/

Also, I am working on a set of Clean modules that implements sets, sequences,
and fnite maps, as used extensvley in all varinats of VDM, and Z.
I intend to release these R.S.N. (honest !)

I am also working on a tool to support Clean <=> LaTeX tranlsation,
for we literate programmers, as well as a .dcl generation program.
I'll release this just as soon as I figure out unique types enough
to make it work  ---- aaaagh !!!


_____________________________________________________________
Andrew Butterfield,                           Location: LG.19
Dept. of Computer Science,               Tel: +353-1-608-2517
O'Reilly Institute,                      Fax: +353-1-677-2204
Trinity College,
Dublin 2, IRELAND.        mailto:Andrew.Butterfield@cs.tcd.ie
URL:                 http://www.cs.tcd.ie/Andrew.Butterfield/