Information Technology Reference
In-Depth Information
heap
h
to show examples of the properties. In these graphs nodes are objects
and edges are labelled with an attribute name. An edge
f
from an object
o
,
h
)=
o
to an object
p
means that
f
(
p
. The edge removed by the heap update
×
.
is depicted as
4.1 Looking at the Heap Before the Assignment
The assignment in (1) may or may not modify the multidot field expression.
Graphically, what matters is whether the edge that has changed belongs to path
followed by the multidot field expression or not. A particular edge is determined
by its object of origin and the field name. Hence, the condition that determines
whether the assignment influences the multidot expression is whether or not the
following set is empty:
=
{
k
:
nat
|
k
<
n
∧
p
=(
g
1
...
g
k
−
1
)(
o
,
h
)
∧
f
=
g
k
}
.
K
pre
We start with the case where
K
pre
is empty, i.e., the edge changed by the assign-
ment is not part of the multidot expression, as shown in Figure 1.
g
n
g
k
=
f
g
n
g
k
g
1
×
×
p
p
o
o
g
k
−
1
f
f
g
1
q
q
(a)
p
=(
g
1
...
g
k
−
1
)(
o
,
h
)
but
f
=
g
k
.
(b)
f
=
g
k
but
p
=(
g
1
...
g
k
−
1
)(
o
,
h
)
.
Fig. 1.
Examples where
K
pre
is empty
As the edge that changed was not part of the multidot expression, the assignment
does have an effect on it.
Property 3.
(
empty
_
K
pre
)
If
K
pre
is empty, then
(
g
1
...
g
n
)(
o
,
h
)=(
g
1
...
g
n
)(
o
,
h
)
.
Now consider the case where
K
pre
is not empty. Figure 2 depicts an example with
two indexes
i
and
k
in
K
pre
such that
k
<
i
. If there are several indexes in
K
pre
,
it means that there are several loops starting at
p
. The assignment breaks the
first edge in these loops. In the heap after the assignment, the edge that joins
p
with
q
is determined by the
least
element in
K
pre
.
Search WWH ::
Custom Search