sean@lfcs.ed.ac.uk (Sean Matthews (AI)) (10/08/88)
I am interested to find out how much interest there is in Formal program
specification techniques in the world.
This is where the formal description of what the program does is
seperated from how it does it; so that instead of being lost in the
detail of implimentation, the designer can concentrate on the
concepts and then prove---using mathematics---that the specification
is free from contradictions, does what it is supposed to do and variou
other properties.
There are two ways that are normally used to do this (apart from the
slightly suspect `specification' languages like logic and fuctional
programming languages):
there is the logic and sets approach of systems like
VDM (the Vienna Development Method)
and
Z (developed by the Programming Research Group in Oxford).
Then there is the algebraic approach of languages like Clear.
these techniques are in use a the moment in some parts of the world for
real development projects. But how much are they in use; I have heard
that IBMs federal systems division uses formal specification techniques in
it `clean room'.
It is my impression that the set theoretic aproach is more common at the
moment, and I think there is a lot of work going on quietly, that I have not
heard about.
Mail me if you yave experience of this sort of technique, if you know
of examples, or if you just have thoughts on the are and if there is
sufficient response I will post a summary.
Se\'an