Lange's Object-Oriented Model

Data structure in the model can be generalized by giving an object-oriented definition, in which data types are combined with operations.

Hyperbase is the top level class for hypertext. Basic operations on instances as the creation of new instances, basic object version management and object access control are covered by hyperbase. These instances are uniquely named, and each has a set of predecessor and successor, the purpose it to identify the neighbors of the instances in the vrsion chain. A collection of uniquely named instances of three object types is called object-oriented hyperbase. These object types are nodes, networks and structures.

Vienna Development Method (VDM)

"The Vienna Development Method (VDM) is a collection of techniques for the formal specification and development of computing systems. It consists of a specification language called VDM-SL; rules for data and operation refinement which allow one to establish links between abstract requirements specifications and detailed design specifications down to the level of code; and a proof theory in which rigorous arguments can be conducted about the properties of specified systems and the correctness of design decisions." [http://www.vienna.cc/evdm.htm]

The VDM is a model-oriented specification language, therefore a specification in VDM consists of a mathematical model. David Lange chose the Vienna Development Method (VDM) because it supports the top-down development of software systems specified in a notion suitable for formal verification.