A survey on formal, object-oriented program development approaches

Due to the popularity of object-oriented programming approaches, there is a growing interest in utilizing object-oriented concepts, such as encapsulation and reuse, when applying formal methods. The main contribution of this paper is to review and compare existing formal methods to develop object-oriented programs from formal specications. The secondary contribution is providing a comparison between widely used object-oriented formal specication languages. The results of this paper can be utilized by researchers wishing to know what open problems are outstanding in the areas of formal, objectoriented specication and program development. Our ndings are also useful for those who are looking for proper specication languages and program development methods to specify and develop object-oriented programs formally. In addition, the provided criteria are suitable for evaluating numerous object-oriented formal specication languages that are under development, either by extending existing formal approaches or formalizing informal OO-methods. As one consequence of this work, it can be mentioned that among formal specication languages, OZ and VDM++ support OO concepts more strongly in comparison to VDM++ and UML-B. Program development methods based on OZ have less tool support. Finally, most proposed methods for formal, object-oriented program development have been evaluated using only case studies, rather than employing formal approaches.