Abstract
Flat VVSL is an extension of a VDM specification language wherein
operations, which interfere through a shared state, can be specified
in a VDM-like style with the use of inter-conditions in addition to
pre- and post-conditions.
Inter-conditions are temporal formulae.
Firstly, this paper explains the role of inter-conditions in the
specification of interfering operations and describes the temporal
formulae that can be used.
Secondly, it describes the interpretation of operation definitions and
temporal formulae in an infinitary logic of partial functions, called
MPLomega.
The purpose of this is to show how a VDM specification language is
semantically combined with a temporal language.
An overview of MPLomega and the VSSL specific aspects of its use for
logical semantics is also given.
Preprint available here.