Modular structuring of VDM specifications in VVSL

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.