Information Technology Reference
In-Depth Information
On page 170 we read:
“We assume that there are no name clashes for local functions [plus local
named rules] between different incarnations of the same rule (i.e. each rule in-
carnation has its own local dynamic functions [and local named rules]).”
Borger and Stark [BoS03] present an inductive definition of the dynamic se-
mantics of Turbo ASM rules in the manner of a derivation calculus for the so
called
yields
-relation
,ζ,U
)
where
E
is an environment of named rules,
Q
is an unnamed rule,
E
yields
(
E
|
Q,
A
|
Q
is
a rule unit,
is a state, i.e. an assignment of values to all locations given by
asignature
Σ
,
ζ
is an assignment to logical variables and
U
is an update set.
The copy rule of Algol60 with its implicit bound renamings is turned into the
following derivation rule for Turbo ASM's call rule (please, be carefull and differ
between “ASM rule” and “derivation rule”):
A
yields
(
E
|
P
t
x
1
,
A
,ζ,U
)
t
n
x
n
...
,ζ,U
)
-where
r
(
x
1
,...,x
n
)=
P
is a named Turbo ASM-rule from the environment
E
in which all rule names
r
are assumed to be pairwisely different,
- where name clashes in the substituted
P
t
x
1
yields
(
E
|
r
(
t
1
,...,t
n
)
,
A
are avoided by implicit
bound renamings of names (identifiers) which are declared and bound
inside
P
.
In case we have a program-like abstract state machine
M
, i.e. one where the
environment does not interfere internal states of
M
, then dynamic semantics of
M
is defined as follows: If
yields
(
E
M
|
t
n
x
n
...
,U
)
with a consistent update set U is derivable then a run of
M
, applied to initial
state
r
M
,
A
,
∅
+
U
.
Since logical variables in the named rules of
E
M
are not free
ζ
is allowed to be
the empty assignment
A
, is called
successfully (regularly) terminating in resulting state
A
∅
.
A Turbo ASM's macro- and micro-computation steps have their analoga in
Algol-implementation. N.G.Fruja and R.F.Stark do an interesting investigation
[FrS03] on the hidden computation steps of Turbo ASMs by the help of so
called PAR/SEQ-trees. So the specification language Turbo ASM has not only a
natural big step operational semantics, defined by the
yields
-relation, there is also
an equivalent small step structural operational semantics [Plo81]. An Algol60-
program corresponds to a purely sequential Turbo ASM. Such a program has
PAR/SEQ-trees as well. They are tail constituents of runtime stack contents of
nested procedure incarnations as we find them in the program's formal execution
tree [Lan73a, Old81a, Lan04].
Furtheron, there is a connecting view of big step operational and denotational
semantics of Algol-programs and Turbo ASMs [Sco70, MiSt76, Bak80]. The de-
notational style to define semantics of a given program or machine
M
with
recursive procedures or named rules is to search for a continuous functional
Φ
Search WWH ::
Custom Search