A survey on formal, object-oriented program development approaches


Faculty of Electrical and Computer Engineering, Shahid Beheshti University G.C., Tehran, Iran


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.