Information Technology Reference
In-Depth Information
1 public static void m(String args[]) {
2 Connection c1 = new Connection(args[0]);
3 Connection c2 = new Connection(args[0]);
4 c1.close();
5 c2.close();
6 c1.write(args[1]);
7 c2.write(args[1]);
………………………
S
8
= ({2},
C
= {
O
2
})
…
8 c2.close();
………………………
T
8
= ({1},
C
= {
O
2
})
F
8
= ({2},
C
≠
{
O
1
})
9 c1.write(args[1]);
………………………
…
F
9
=
({2},
T
)
10 c2.write(args[1]);
11 }
Fig. 2.
The example for motivating the first optimization
The variable binding specifies the static objects [9] which represent the concrete
runtime objects. Actually, for a shadow
s
, it also has a variable binding [8] spec-
ifying the objects whose typestates can be changed by
s
. Two variable bindings
are
compatible
if they can be bound to a same static object or a same group
of related static objects. A configuration and a shadow are
compatible
if their
variable bindings are compatible. For a statement
st
associated with a configu-
ration (
Q,b
), in forward analysis, the elements in set
Q
represent all the possible
states which the static objects specified by the variable binding
b
can reach just
before
st
; in backward analysis, they are the states from which the static objects
specified by
b
can reach a final state via the execution after
st
. For example, the
configuration
S
8
in Figure 2 represents that the static object
O
2
can reach state
2 before executing line 8. The configuration
F
12
in Figure 3 represents that the
static object
O
can reach the final state from state 0 or 1 via the execution after
line 3.
Providing that the program creates the compile-time static objects
O
1
and
O
2
at line 2 and line 3, respectively. The variable binding of the shadow at line
8is
C
=
{
O
2
}
, and the shadow at line 8 changes the configuration from
S
8
=
(
{
2
}
,C
=
{
O
2
}
)to
T
8
=(
{
1
}
,C
=
{
O
2
}
) in the forward analysis, with respect
to the typestate property.
F
8
=(
) associated to the shadow at
line 8 is one of the resulting configurations produced by the backward analysis
starting at line 9, which means the typestate of the object does not change if
the object is not
O
1
. The variable bindings of
S
8
and
F
8
are both compatible to
that of the shadow at line 8. According to the “nop shadow” conditions, because
the states of the state transition caused by the shadow at line 8,
i.e.
, state 2 in
S
8
and state 1 in
T
8
, are not both contained in the state set
{
2
}
,C
=
{
O
1
}
{
2
}
of
F
8
, NSA fails
to identify this shadow as a “nop shadow”.
Actually, the configuration
F
8
is induced by the “final shadow”
1
at line 9,
in which the variable
c
1
is totally unrelated to the variable
c
2
at line 8,
i.e.
,
1
“final shadow”, which can drive the FSM of the property into a final state [6].
