VDM++, a formal specification language for object-oriented designs

Abstract

Some general issues in the design of VDM++ are discussed. VDM++ extends VDM by offering classes, objects and inheritance and provides as an additional feature, a formalism to specify the allowed invocation sequence of methods. The design of VDM++ is such that any specification in VDM++ can be translated automatically into a specification in classical flat VDM, as defined in BSI/IST/5/50, thereby implicitly defining the semantics in terms of the semantics of VDM.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">&gt;</ETX>