Information Technology Reference
In-Depth Information
Property 2.
If
p
=
o
and
f
=
g
,then
g
(
o
,
(
:=
)(
p
,
h
)) =
q
.
f
q
The proofs of these two properties amount to expanding the definition of
and
applying several case-splits. When the assignment is replaced with a qualified
assignment
e
1
f
:=
e
2
, then analogous properties hold, but
p
=
o
is replaced by
e
1
(
o
,
h
)=
o
.
One has to explicitly apply properties 1 and 2 as proof steps to reason about
the effect of an assignment in the presented semantics. The key condition is
p
:=
g
. The latter is a syntactical comparison and thus can be done au-
tomatically. However, most of the time comparison between objects cannot be
discharged automatically, unless we have information about the layout of the
heap, see Section 6.
=
o
∧
f
=
4
The Effect of Assignments on Multidot Expressions
In this section we look at expressions of the form
(
g
1
...
g
n
)(
o
,
(
:=
)(
p
,
h
))
,
(1)
f
q
where the
g
i
and
f
are field names,
o
and
p
are
Object
v
⊥
and
q
is of type
Object
v
.
Because undefinedness due to dereferencing void is not an essential part of the
discussion, we shall omit it in the rest of the paper.
Properties 1 and 2 describe the result of a very simple multidot, namely
one where
n
is equal to
. There, the condition which determines the result is
p
=
o
∧
f
=
g
. In multidot field expressions of arbitrary length a similar condition
determines the result, but now it must be taken into account that in the path
from
o
to
1
, the field
f
of the object
p
can be
traversed more than once if there is a loop. Thus we are interested in the set of
indexes
k
such that:
(
g
1
...
g
n
)(
o
,
(
f
:=
q
)(
p
,
h
))
p
=(
g
1
...
g
k
−
1
)(
o
,
h
)
and
f
=
g
k
.
The properties we present in this section are categorised into
separation rules
,
where the assignment has no effect on the multidot field expression, and
interfer-
ence rules
, where the assignment does have effect on the multidot field expression.
Moreover, we now have a choice to look at the heap
h
before the assignment, or at
the heap
h
=(
f
:=
q
)(
p
,
h
)
after the assignment. For the separation properties
this does not make a difference, but for the interference properties it does.
The properties we derive about multidot expressions in this section are at
the meta-level. Although it is possible to use them to reason about a particular
multidot in a program, the intended use is to reason about the effects of assign-
ments on recursive data structures. Examples that demonstrate the application
are given in Section 5.
To improve readability, the notation for multidot expressions differs from the
actual syntax used in PVS. In the last subsection we show the concrete PVS
formalisation of a property. We will use graphs representing a portion of the
Search WWH ::
Custom Search