How can theoretical techniques of logical code analysis and specification be applied by software engineers to maintain and extend mature software systems? Existing techniques for logical code analysis and specification, based on weakest precondition calculations, have been developed by Dijkstra, Gries, and others, but practical use of these techniques has always been limited and is generally confined to program development. This paper discusses our successful experience applying these techniques to existing software. Our success depends upon a combination of training software engineers, learning how and when to apply the techniques, and the fact that we are working with existing code rather than creating new systems. The objective is to learn how to apply these techniques to software so as to improve quality and productivity and to extend useful product life.
展开▼
