VDM Semantics of Programming Languages: Combinators and Monads - Formal Methods and Hybrid Real-Time Systems - page 483

VDM Semantics of Programming Languages:
Combinators and Monads

Peter D. Mosses

Department of Computer Science, Swansea University, UK
[e-mail]
http://www.cs.swan.ac.uk/ ∼ cspdm/

Abstract. Although VDM semantic descriptions of programming lan-
guage are denotational, they can be read quite operationally. After re-
calling the main features of denotational semantics, this paper examines
the combinators of the VDM specification language, and relates them to
the use of monads in the monadic style of denotational semantics. It also
provides an overview of published VDM semantic descriptions of major
programming languages. Familiarity is assumed with the basic concepts
of formal specification.

1 Introduction

The Vienna Development Method, VDM, is a major framework for the formal
specification and rigorous development of software systems. In this paper, we
focus on the use of VDM for semantic description of programming languages,
which was the original motivation for the framework.
VDM evolved from the operational semantics framework known as VDL, the
Vienna Definition Language [1], in the early 1970s [2]. The main change in the
transition from VDL to VDM was the adoption of the fundamental principles
of denotational semantics, which had already been established by Scott and
Strachey [3]. One of the innovations in the VDM style of denotational semantics
was the introduction of a number of combinators having a fixed operational
interpretation. We shall see that these combinators are closely related to the
operations that later formed the basis for the monadic style of denotational
semantics.
The rest of the paper proceeds as follows: Section 2 recalls the fundamen-
tal principles of denotational semantics. Section 3 illustrates the original style
adopted in denotational descriptions at Oxford, both before and after the intro-
duction of continuations. Section 4 illustrates the VDM style, and explains the
main differences between it and the Oxford style. Section 5 presents the concepts
and notation used in the monadic style of denotational semantics, and examines
the claim that VDM is actually based on monads. Section 6 gives an overview
of published VDM semantic descriptions of major programming languages, and
proposes to establish an online repository for semantic descriptions of program-
ming languages in all frameworks. A concluding section summarises the main