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

[[ ε 0 ]] ( ρ ) ˆ [[ ε 1 ]] ( ρ ) ˆ C [[ ε 0 := ε 1 ]] = λρ. E ∗ λβ 0 . E ∗ λβ 1 .Assign ( β 0 | L, β 1 ) (9)

This minor change of notation allows the terms to be read more operationally,
from left to right, with the λ -abstractions simply naming the values computed
by the preceding terms. (It also substantially reduces the number of required
parentheses.) In Sect. 5 we shall compare the above formulation with the monadic
style.

Continuation Semantics. Scott and Strachey's original denotations for com-
mands and expressions, based on store transformers, can represent both normal
termination and nonterminating behaviour. To represent abrupt termination,
due to escapes (such as break or return) and jumps to labels, the denotations
need to be enriched. The standard technique in the Oxford style (often used
also for languages that do not involve abrupt termination) is to replace store
transformers by continuation transformers, where continuations are themselves
some kind of store transformers [15]. The semantics of abrupt termination in-
volves ignoring the argument continuation and applying a different one. As we
shall see in the next section, the VDM style avoids the use of continuations by
letting store transformers return extra values that indicate whether termination
is normal or abrupt, and by introducing combinators to propagate and detect
the extra values; see [16] for a detailed comparison of the two techniques.
Any ordinary store transformer θ can be converted to a continuation trans-
former which, given a continuation θ , returns the continuation that maps any
store σ to the result of θ ( θ ( σ )). This continuation transformer can be expressed
by λθ .θ ◦

θ . The original store transformer can be retrieved from the continua-
tion transformer by applying it to the identity continuation.
Denotations of commands map environments to continuation transformers:

C : Cmd → Env → C → C (10)

where the domain C of command continuations θ can be defined as C = S S .

The denotation of command sequencing using continuations is defined as follows:

→

C [[ γ 0 ; γ 1 ]] = λρ.λθ. C [[ γ 0 ]] ( ρ ) {C [[ γ 1 ]] ( ρ ) { θ }}

= λρ.

C

[[ γ 0 ]] ( ρ )

◦C

[[ γ 1 ]] ( ρ )

(11)

C :the
continuation is to be applied to the value of the expression. Denotations of
expressions are given by the semantic function:

The domain of expression continuations κ is defined as K = V →

E : Exp → Env → K → C (12)

The continuation semantics of conditional commands is defined by:

C [[ ε -> γ 0 , γ 1 ]] = λρ.λθ. E [[ ε ]] ( ρ ) { λβ.Cond ( C [[ γ 0 ]] ( ρ ) , C [[ γ 1 ]] ( ρ ))( β | T ) { θ }}

= λρ. E [[ ε ]] ( ρ ) ◦ λβ.Cond ( C [[ γ 0 ]] ( ρ ) , C [[ γ 1 ]] ( ρ ))( β | T ) (13)

and that of assignment commands by:

C [[ ε 0 := ε 1 ]] =