The VIP VDM specification language

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. VVSL was designed and is being used in the ESPRIT project 1283: VIP. 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 mainly by a linear, discrete time temporal logic from Lichtenstein, Pnueli and Zuck that includes operators referring to the past. VVSL is provided with a well-defined semantics by defining a translation to an extension of COLD-K (which has itself a well-defined semantics). 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 given too. These examples are based on a formal definition of the relational data model. With respect to the constructs for expressing temporal aspects, only the semantic ideas underlying the use of temporal formulae in VVSL are briefly outlined.