89
fect of those changes, and thus the content of A’(S) is significantly modified by the ordering
of the addresses, since move, copy and delete all specify their regions of effect in terms of
the endpoints of ranges of addresses. Because of this, it is necessary to be careful to avoid
circular definitions. This is achieved by defining an ordering over all syntactically legal ad-
dresses that can be created from a change set. The effects of those changes are then defined
in terms of the ordering of the larger set. The effects in question, in this case, are the set of
legal addresses in the sequence, and the contents of the ranges between the legal addresses.
Only with these definitions in place can a consistent definition be given of which members
of A(S)are not included inA’(S) .
A(S),whereSis a minimally consistent change set, is the set of all addresses satisfying
Definition 4.1 and constructed using only the IDs of changes inS. We will define the order-
ing relation <
SA on the set A(S), and will later restrict it to the setA’(S) ˝ A(S). In defining
<
SA , we will need to define another relationship between addresses. The refersrelation allows
us to order changes with respect to the other changes referred to by the destination of the
initial change in their change paths.
Definition 4.6:The destination relation<
d is defined on addresses as follows:
1. Fora = (I
1 …I
n , i), b = (I’
1 …I’
n , j), a <
d biffI
1 e Ids(Dest(I’
1 ))
2. Ifa <
d b,andb <
d c,thena <
d c.
Lemma 4.1:Fora = (I
1 …I
n , i), b = (I’
1 …I’
n , j), a <
d biffI
1 <
r I’
1 .
Proof:To show the forward direction (a <
d bimplies thatI
1 <
r I’
1 ) we only need to observe
that I
1 e Ids(Dest(I’
1 ))implies thatChange(I
1 ) e Refs(I’
1 ),and thusI
1 <
r I’
1 by Definition4.3.
In the other direction, assume that I
1 <
r I’
1 and it is not true that a <
d b.Then must be a
counterexample, an address x = (I’’
1 …I’’
n , k)such thatI
1 £
r I’’
1 <
r I’
1 , and for which a £
d xor
x <
d bis false. This means either thatx „ aandI
1 ˇ Ids(Dest(x))orI’’
1 ˇ Ids(Dest(b)). But
fect of those changes, and thus the content of A’(S) is significantly modified by the ordering
of the addresses, since move, copy and delete all specify their regions of effect in terms of
the endpoints of ranges of addresses. Because of this, it is necessary to be careful to avoid
circular definitions. This is achieved by defining an ordering over all syntactically legal ad-
dresses that can be created from a change set. The effects of those changes are then defined
in terms of the ordering of the larger set. The effects in question, in this case, are the set of
legal addresses in the sequence, and the contents of the ranges between the legal addresses.
Only with these definitions in place can a consistent definition be given of which members
of A(S)are not included inA’(S) .
A(S),whereSis a minimally consistent change set, is the set of all addresses satisfying
Definition 4.1 and constructed using only the IDs of changes inS. We will define the order-
ing relation <
SA on the set A(S), and will later restrict it to the setA’(S) ˝ A(S). In defining
<
SA , we will need to define another relationship between addresses. The refersrelation allows
us to order changes with respect to the other changes referred to by the destination of the
initial change in their change paths.
Definition 4.6:The destination relation<
d is defined on addresses as follows:
1. Fora = (I
1 …I
n , i), b = (I’
1 …I’
n , j), a <
d biffI
1 e Ids(Dest(I’
1 ))
2. Ifa <
d b,andb <
d c,thena <
d c.
Lemma 4.1:Fora = (I
1 …I
n , i), b = (I’
1 …I’
n , j), a <
d biffI
1 <
r I’
1 .
Proof:To show the forward direction (a <
d bimplies thatI
1 <
r I’
1 ) we only need to observe
that I
1 e Ids(Dest(I’
1 ))implies thatChange(I
1 ) e Refs(I’
1 ),and thusI
1 <
r I’
1 by Definition4.3.
In the other direction, assume that I
1 <
r I’
1 and it is not true that a <
d b.Then must be a
counterexample, an address x = (I’’
1 …I’’
n , k)such thatI
1 £
r I’’
1 <
r I’
1 , and for which a £
d xor
x <
d bis false. This means either thatx „ aandI
1 ˇ Ids(Dest(x))orI’’
1 ˇ Ids(Dest(b)). But
