Abstract
VVSL is a language for writing modularly structured VDM specifications.
Its modularization mechanism permits two modules to have parts of
their state in common, including hidden parts.
Firstly, this paper gives an overview of the structuring sublanguage
of VVSL and a concise description of its semantic foundations:
DA (a general algebraic model of modules) and lambda-pi-calculus
(a variant of classical lambda calculus).
The paper also presents a variation on a `challenge problem' of
Fitzgerald and Jones as an example of the use of VVSL's structuring
language.
Finally, their modular structuring style and the suggested language
features to support it are commented.
View-only version of article
Preprint available here.