Information Technology Reference
In-Depth Information
5.2
Denotations
Let us conclude this section by showing how simple it can be to define the
denotations of our illustrative phrases in the monadic style. We shall not bother
to define the monad T , since the details of the definition do not affect how
denotations are expressed, nor their operational understanding. We do however
assume that T is both a side-effect monad and an environment monad.
Thesemanticfunction
maps commands to their denotations in T (), since
commands do not compute values (which is represented by computing the null
value).
C
C
: Cmd
T ()
(19)
The semantic function
maps expressions to their denotations in T ( V ), where
V is a domain of values whose definition depends on the language being de-
scribed, but is here assumed to include both L (locations) and T (truth values)
as summands.
E
E
: Exp
T ( V )
(20)
Thanks to the use of monadic notation, the denotations of various commands
and expressions can be defined without notational clutter regarding appropri-
ate propagation of the environment ρ and the store σ (not to mention details
concerning the representation of abnormal termination):
C
[[ γ 0 ; γ 1 ]] =
C
[[ γ 0 ]] >> = λ () .
C
[[ γ 1 ]]
(21)
C
[[ ε -> γ 0 , γ 1 ]] =
E
[[ ε ]] >> = λβ. Cond (
C
[[ γ 0 ]] ,
C
[[ γ 1 ]] ) ( β
|
T )
(22)
C
[[ ε 0 := ε 1 ]] =
E
[[ ε 0 ]] >> = λβ 0 .
E
[[ ε 1 ]] >> = λβ 1 . Update ( β 0 |
L, β 1 )
(23)
The reader is invited to compare the above semantic equations with those given
in the Oxford style (Sect. 3) and in the VDM style (Sect. 4). The basic monadic
combinators provided in both those early styles allowed them to get close to
the simplicity of the monadic style. VDM has the advantage of a fixed opera-
tional interpretation for its combinators, and originally used what is essentially
a monad transformer when adding the possibility of abnormal termination.
6
Published VDM Semantic Descriptions
VDM was originally developed for giving a formal definition of PL/I and pro-
viding a formal basis for the development of a compiler [2]. Other major pro-
gramming languages that have been described using VDM include Algol 60,
Pascal, Ada, and Modula-2. The aim here is merely to give a general overview of
the cited descriptions. In general, the descriptions are out of print; this section
concludes by proposing the establishment of an online repository for semantic
descriptions, so that these major contributions can be preserved and made more
easily accessible to the research community.
 
Search WWH ::




Custom Search