Content area
Full text
KEYWORDS
Formal program development; Object-orientation; Formal specification; Object-Z; VDM; VDM++; B; Event-B; UML-B.
Abstract. 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 specifications. The secondary contribution is providing a comparison between widely used object-oriented formal specification languages. The results of this paper can be utilized by researchers wishing to know what open problems are outstanding in the areas of formal, object-oriented specification and program development. Our findings are also useful for those who are looking for proper specification 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 specification 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 specification 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.
© 2015 Sharif University of Technology. All rights reserved.
(ProQuest: ... denotes formulae omitted.)
1. Introduction
In the late 1960s, formal methods based on mathematics were proposed as an option for providing software reliability [1]. Formal methods are used to uncover ambiguity, incompleteness and inconsistency in a system. These methods can be used at any stage of software development, from the initial statement of a customer's requirements to system implementation and verification. Usually, these methods are introduced to the software life-cycle by adding the formal specification stage to the stages of software projects. At this stage, we describe WHAT has to be done in the final software, instead of HOW it has to be done.
Formal program development is a process producing software program code in relatively high level programming languages, such as C and Java, from a given formal specification of the software. A formal program development process has two stages. First, programs are specified using...