Information Technology Reference
In-Depth Information
{
E[((
λx.M
)
V
)]
m
{
E[
{x → V }M
]
m
Σ
W
},T,S−−→
E
},T,S
Σ
{
E[(if
tt
then
N
t
else
N
f
)]
m
{
E[
N
t
]
m
W
},T,S−−→
E
},T,S
E[(if
ff
then
N
t
else
N
f
)]
m
{
E[
N
f
]
m
Σ
W
},T,S−−→
E
},T,S
{
E[(
V
;
N
)]
m
{
E[
N
]
m
Σ
W
},T,S−−→
E
},T,S
Σ
{
E[(
x.X
)]
m
E
{
E[(
{x →
(
x.X
)
} X
)]
m
W
},T,S−−→
},T,S
{
E[(flow
F
in
V
)]
m
{
E[
V
]
m
Σ
W
},T,S−−→
E
},T,S
Σ
{
E[(!
a
)]
m
{
E[
S
(
a
)]
m
W
},T,S−−→
E
},T,S
Σ
{
E[(
a
:=
V
)]
m
{
E[()]
m
W
},T,S−−→
E
},T,
[
a
:=
V
]
S
{
E[(ref
θ
V
)]
m
{
E[
a
]
m
Σ
W
},T,S−−→
E
},T,
[
a
:=
V
]
S,afresh in S
and Σ
(
a
)=
θ
W
(
T
(
m
))
F
W
Σ
{
E[(allowed
F
then
N
t
else
N
f
)]
m
},T,S −→
E
{
E[
N
t
]
m
},T,S
W
(
T
(
m
))
F
W
Σ
{
E[(allowed
F
then
N
t
else
N
f
)]
m
},T,S −→
E
{
E[
N
f
]
m
},T,S
W
Σ
{
E[(thread
N
at
d
)]
m
},T,S−−→
E
{
E[()]
m
,N
n
},
[
n
:=
d
]
T,S,
n fresh in
T
Σ
P,T,S
F
P
,T
,S
P ∪ Q,T,S is well formed
W
W
Σ
P ∪ Q,T,S
F
P
∪ Q,T
,S
Fig. 2.
Operational Semantics
We write E[
M
] to denote an expression where the sub-expression
M
is placed
in the evaluation context E, obtained by replacing the occurrence of [] in E by
M
. The flow policy that is permitted by the evaluation context E is denoted by
. It consists a lower bound (see Section 2) to all the flow policies that are
declared by the context:
E
[]
=
,
(flow
F
in E)
=
F
E
,
(2)
E
[E]
,
when
E
does not contain flow declarations
=
E
The following basic notations and conventions are useful for defining transi-
tions. For a mapping
Z
, we define dom(
Z
) as the domain of a given mapping
Z
.
We say a name is fresh in
Z
if it does not occur in dom(
Z
). We denote by rn(
P
)
and dn(
P
) the set of reference and domain names, respectively, that occur in the
expressions of
P
.Weletfv(
M
) be the set of variables occurring free in
M
.We
restrict our attention to well formed configurations
P,T,S
satisfying the con-
ditions that rn(
P
)
⊆
dom(
S
), that dn(
P
)
⊆
dom(
W
), that dom(
P
)
⊆
dom(
T
),
and that, for any
a
∈
dom(
S
), rn(
S
(
a
))
⊆
dom(
S
) and dn(
S
(
a
))
⊆
dom(
W
).
