Object-oriented formal specification development using VDM

Abstract

This paper introduces the Object-Oriented Specification Language, a language based on Formal Description Technique (FDT) in the style of Vienna Development Method (VDM) so called OOVDM, additionally includes its denotational semantics and implementation. Our research contributes to the extension of VDM by an Object-Oriented concept which supports incremental & subtyping inheritance. OOVDM has two types of modules, which are class modules and type modules. Class modules define objects having their internal states. Their states can be changed by the execution of the operations on them. Type modules specify objects with no states, i.e. values, and denote the domains of the values. OOVDM has two kinds of inheritance mechanisms — incremental inheritance and subtyping inheritance. Both concepts are useful for overloading existing descriptions and for hierarchical classification of the objects.