Abstract
In VVSL, a language for structured VDM specifications is combined with a language of temporal logic in order to support implicit specification of 'non-atomic operations', i.e. procedures whose behaviour depends on the interference of concurrently executed procedures through state variables.
In this paper the role of temporal formulae in VVSL is explained and an overview is given of the language of temporal logic that can be used in
VVSL.
Electronic version.