A Unified Systems Development Paradigm Which Synthesises Object-Oriented Methodologies and VDM

This work describes a methodology for systems development whereby the techniques of object-oriented analysis and design are synthesised with those of VDM, a formal development method. The methodology involves the use of Object-Oriented Analysis to derive an Object-Oriented/VDM specification; this specification is then used as the basis for a design technique which synthesises object methods with the formal development techniques of VDM, namely Data Reification and Operation Decomposition.
The work shows that all the important concepts which together define Object-Orientation can be captured in VDM. It demonstrates how the notion of encapsulation can be represented by the use of the VDM module; how inheritance relationships can be represented by means of the module import and export sections; how message-passing between objects can be specified by the quoting of pre- and post-conditions; and how polymorphic relationships can be represented by the use of the parameterised module notation of VDM.
The work also shows how the behaviour of inherited classes can be proved to be consistent by the application of VDM proof obligations.
It is intended that this methodology should make formal methods more accessible to the practitioner, since it does not involve adaptations to the language, but rather demonstrates that the existing VDM development methods easily lend themselves to use in an object-oriented world.