Information Technology Reference
In-Depth Information
In contrast, each combinator used in the Oxford style has a
fixed definition
, but
its operational interpretation varies. For example, the VDM combinator writ-
ten '
s1;s2
' always represents sequential composition of state transformations,
(starting from
s1
, and continuing with
s2
when
s1
terminates normally) and
its definition depends on that of the domain of state transformations; in the
Oxford style, the combinator
f
g
is defined as an abbreviation for
λx.f
(
g
(
x
)),
and what it represents operationally varies, as illustrated in Sect. 3.3.
The abbreviation '
=>
' in VDM stands for the domain of pure transformations,
and '
=>R
' stands for the domain of transformations that return values in
R
.
The domain of functions from
D
to
=>
is written
D=>
; similarly, the domain of
functions from
D
to
=>R
is written
D=>R
. Below, assume
s
is in
=>
,
e
is in
=>V
,
and
f
is in
V=>
or
V=>R
.
The main imperative combinators used in the VDM style of denotational
semantics are as follows:
◦
-
sequencing '
def x: e; f(x)
' applies the transformation
e
, followed by the
transformation obtained by applying
f
to the value
x
returned by
e
;
-
'
return v
' simply returns the value
v
without transforming the state;
-
'
I
' is the identity transformation on states;
-
assignment '
r:=e
' first applies
e
, then replaces the component of the state
selected by
r
by the value returned by
e
;
-
contents '
c r
' returns the component of the state selected by
r
without
transforming the state;
-
sequencing '
s1; s2
' applies
s2
to the state obtained by applying
s1
;
-
conditional '
if b then s1 else s2
' applies
s1
or
s2
, depending on whether
the boolean value
b
is
true
or
false
;
-
iteration '
for i=mtondos(i)
' abbreviates '
sm;...;sn
'.
Some further combinators are used in connection with abrupt termination:
-
'
exit v
' terminates abruptly, returning a non-
nil
abnormal value
v
;
-
'
trap x with f(x) in s
' handles abrupt termination of
s
with the trans-
formation obtained by applying
f
to the abnormal value
x
returned by
s
;
-
'
tixe mins
' handles abrupt termination of
s
by applying the transforma-
tion to which the abnormal value returned by
s
is mapped by
m
(repeatedly),
propagating the abrupt termination if the value is not in the domain of
m
;
-
'
always s2 in s1
' applies
s1
, then applies
s2
, regardless of whether ter-
mination of
s1
was normal or abnormal (
s2
is not supposed to terminate
abnormally).
All the above combinators are defined by translation to
λ
-notation, making
the state explicit. In the absence of abrupt termination, '
=>
'and'
=>V
'are:
→
STATE
=>V = STATE
˜
= STATE
˜
=>
→
×
STATE
V
When the possibility of abrupt termination is introduced, '
=>
' is redefined as:
= STATE
˜
→
STATE
×
[
ABNORMAL
]
=>
Search WWH ::
Custom Search