VVSL: A language for structured VDM specifications

Abstract

VVSL is a VDM specification language of the “British School” with modularisation constructs allowing sharing of hidden state variables and parameterisation constructs for structuring specifications, and with constructs for expressing temporal aspects of the concurrent execution of operations which interfere via state variables. The modularisation and parameterisation constructs have been inspired by the “kernel” design language COLD-K from the ESPRIT project 432: METEOR, and the constructs for expressing temporal aspects by various temporal logics based on linear and discrete time. VVSL is provided with a well-defined semantics by defining a translation to COLD-K extended with constructs which are required for translation of the VVSL constructs for expressing temporal aspects. In this paper, the syntax for the modularisation and parameterisation constructs of VVSL is outlined. Their meaning is informally described by giving an intuitive explanation and by outlining the translation to COLD-K. It is explained in some detail how sharing of hidden state variables is modelled. Examples of the use of the modularisation and parameterisation constructs are also given. These examples are based on a formal definition of the relational data model. With respect to the constructs for expressing temporal aspects, the ideas underlying the use of temporal formulae in VVSL are briefly outlined and a simple example is given.