Information Technology Reference
In-Depth Information
11. local rule with local named block with local procedures,
rules and functions
simple variables and arrays
12. named rule with formal
procedure declaration with formal
parameters
call-by-name parameters
13. body as right hand side
procedure body
of a named rule
14. call rule procedure statement or call
15. formal call rule formal procedure statement or call
16. actual parameter actual call-by-name parameter
These language constructs, cum grano salis, are already available in Basic ASM,
but Turbo ASM has a considerably richer semantics. Namely, Basic ASM does
not allow that submachines (named rules) may call themselves recursively.
I.e. submachines and phrases 11. to 16. are used only as a notational macro-
shorthand in Basic ASM.
The syntax of an abstract state machine
M
consists of three components, 1. a
signature (vocabulary)
Σ
M
, 2. a set (an environment)
E
M
of named rule declara-
tions and 3. a distinguished 0-ary main rule name
r
M
. Static semantics requires
that every free function name is used due to its classification in
Σ
M
and that
there are no free logical variables (let-variables etc.). In order to demonstrate
close neighbourhood of Algol60 and Turbo ASM we present the Algol60-program
example
π
2
of section 2.2 in the shape of two named rules in
E
M
π
2
:
{
local q(r,s) =
p(f,g) =
{
}
print(g)
}
f(q,false)
}
We interprete the transition from Basic ASM to Turbo ASM with its named
recursive rules as a clear indication that ASM has taken over aspects of VDM's
specification style, see [BjJ78, Jon89].
r
M
π
2
=
{
p(p,true)
3.2
Dynamic Semantics
The informal semantics and execution explanation of procedures and their calls
in Algol60 (see the copy rule sections 4
.
7
.
3
.
2and4
.
7
.
3
.
3 in [Nau60, Nau63] and
in subsection 2.1 of this essay) and of named rules and their calls (see pages 73
and 170 in [BoS03]) are very similar although there is no explicit mentioning of
the Algol60-report in [BoS03]. On page 73 we read:
“Rules [
r
(
x
1
,...,x
n
)=
P
] are called
by name
. This means that in a call
r
(
t
1
,...,t
n
) the [ free occurrences of the ] variables
x
1
,...,x
n
are [textually]
replaced in the body
P
by the parameters
t
1
,...,t
n
. The parameters are not
evaluated in the state where the rule is called, but only later when they are
used in the body .... In the extension of ASMs each formal parameter of a
rule declaration is either a logical variable ...or a location variable or a rule
variable.”
Search WWH ::
Custom Search