Hardware Reference
In-Depth Information
SF9 flow
.X; r
[+]
/
D
flow
.X; r
[
*
n
]
/
D
flow
.X; r/, provided n is positive.
Analogous equalities apply to ranged forms of the repetition operator, provided
the lower range is positive. If the lower range is zero, then the flow rule is
obtained by decomposing r
[
*
0:
n
]
as r
[
*
0]
or
r
[
*
1:
n
]
(n positive or
$
).
22.6.2
Local Variable Contexts
The principal technical device introduced to define the semantics of local variables
is the local variable context. A
local variable context
is a partial function mapping
local variables to values. It can be written as a set of ordered pairs:
L
Df
.
v
1
;a
1
/; .
v
2
;a
2
/;:::;.
v
n
;a
n
/
g
L specifies that for each i , 1
i
n, the local variable
v
i
is assigned and has
the value a
i
. It is customary to say that
f
v
1
;
v
2
;:::;
v
n
g
is the
domain
of L, written
dom.L/. Thus, the domain of a local variable context is the set of local variables
that are assigned in that context. Any local variable not in the domain of the local
variable context is unassigned in that context. A local variable context may be
empty, in which case its domain is also empty and all local variables are unassigned
in that context.
If D
dom.L/, then L
j
D
denotes the local variable context obtained by
restricting L to the domain D. For example, with L as above and D
Df
v
1
;
v
3
g
,
L
j
D
Df
.
v
1
;a
1
/; .
v
3
;a
3
/
g
L
n
v
denotes L
j
dom.L/
f
v
g
. It is the local variable context that results from L by
removing
v
from the domain, if it was there to begin with.
22.6.3
Sequence Semantics with Local Variables
The semantics of matching (i.e., tight satisfaction) of unclocked sequences can now
be defined as a four-way relation:
w
;L
0
;L
1
j
r
The relation holds if r matches the finite word
w
starting with incoming local
variable context L
0
and resulting in outgoing local variable context L
1
. Whenever
the relation holds, dom.L
1
/
D
flow
.dom.L
0
/; r/. This fact is proven in [
41
]. The
substance of defining the relation is to capture how the local variable contexts
evolve, as a result of assignments to local variables, local variables becoming
unassigned according to the flow rules, and inductively through intermediate local
variable contexts. Here are the definitions for basic sequence operators:
Search WWH ::
Custom Search