Date: Fri, 12 Apr 96 13:07:30 BST
Position statement on formal methods: Cliff B Jones
Formal methods have been being actively pursued for something over thirty years and even the specific topic of denotational semantics has been around for a quarter of a century. It seems it would be useful to take stock of where we are. At one level we must concede that formal methods have not completely revolutionised the software industry: many practising programmers are completely unaware of the usefulness of formal methods. (Part of the problem is that the tasks associated with the word "programmer" are now much wider than could have been foreseen quarter of a century ago.) In contrast (as someone who has been working on formal methods for a fair proportion of this time) I must say that many of the ideas have been taken up in a far wider community than seemed likely in the early days.
There are two major directions in which one can look at work on formal methods: there is the work on underlying concepts and there is the attempt to apply these concepts to actual problems.
Under the heading of underlying concepts, we look at ideas like process algebra and admire the way extremely complicated facets of operating systems and distributed computing can be summarised using a very sparse set of operators. This work is necessary in order to be able to analyse fundamental problems such as deadlock. Personally I think there is every reason to be pleased with the work which has gone on in this area of fundamental concepts but I do sometimes wonder whether too much of the talent in the PhD community has been spent on continually refining these concepts.
There is an enormous range of potential applications for formal methods which have not on the whole received the attention they might have done. One looks around and sees new sorts of languages every day. I don't just mean object-oriented languages! I mean languages with fundamentally different modes of computation such as Java, languages with different forms of discourse such as those that control robots or provide frameworks for virtual reality systems. Not only would I like to see some of the bright young PhD students work on these application problems, I would also like to see them develop "theories" which made it easier for other people to tackle future languages of this sort. One of my arguments for encouraging young people to look at real application problems is that I believe the "devil is often in the detail" in the sense that one needs to be aware of the pitfalls of the process of abstraction as well as the fundamental mathematical concepts which lie behind those abstractions.
The tests for a useful formal method must include tractability (C provides a formal language but it is not one we wish to do proofs about!); usability (there is no point in telling programmers they must learn Topos theory in order to develop a payroll program!); and wide applicability (it is simply not possible to have one approach which works for stacks and a totally different form of mathematics which is required in order to talk about database systems).
Recent references which support the line of argument above include:
"Some practical problems and their influence on semantics", C. B. Jones, (pp 1--17), in ESOP'96 Proceedings, Lecture Notes in Computer Science Vol. 1058, Springer-Verlag", 1996.
"A Rigorous Approach to Formal Methods", C.B. Jones, IEEE, Computer, Vol. 29, No. 4, pp. 20--21, 1996