A High Productivity Tool for Formally Veri ed Software Development
D. Crocker, Judith Carlton · 2006
It is our view that reliability cannot be guaranteed in large, complex software systems unless formal methods are used. The challenge is to bring formal techniques up to date with modern object-oriented approaches to software design and to make their use as productive as informal methods. We believe that such a challenge can be met and we have developed the Escher Tool to demonstrate this. This paper describes some of the issues involved in marrying formal methods with an object-oriented approach, design decisions we took in developing a language for object-oriented speci cation and re nement, and our results in applying the tool to small and large projects.