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 given too. 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.
View-only version of article
Preprint available here.