Specification of interfering programs based on interconditions

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 by the use of interconditions in addition to pre- and postconditions. Interconditions are temporal formulae. The paper explains the role of interconditions in the specification of interfering operations and describes the temporal formulae that can be used. It also describes the interpretation of operation definitions and temporal formulae in an infinitary logic of partial functions called MPI_ω. The purpose of this is to show how a VDM specification language is semantically combined with a temporal language. An overview of MPI_ω and the VVSL-specific aspects of its use for logical semantics is also provided