Reasoning about Assignments in Recursive Data Structures - Formal Methods: Foundations and Applications - page 168

g i − 1

g k + 1

f = g ×

p

o

f = g i

g k − 1

g 1

g k + 1

g i g n

q

Fig. 2. Example with two indexes k < i in K pre

Property 4. ( min _ K pre ) If k = min ( K pre ) ,then

( g 1 ￿ ... ￿ g n )( o , h )=( g k + 1 ￿ ... ￿ g n )( q , h )

.

Since the assignment may also affect the path that goes from q to the final value,
the right hand side must still be evaluated in h .

4.2 Looking at the Heap After the Assignment

Instead of looking at when the multidot expression follows the edge that changed
in h , we will now look at when it follows the new edge in h . That is, we will
look at the set:

= { k : nat | k < n ∧ p =( g 1 ￿ ... ￿ g k − 1 )( o , h ) ∧ f = g k } .

K pos

If the new edge is never traversed, the multidot expression does not change.

Property 5. ( empty _ K pos ) If K pos is empty, then

( g 1 ￿ ... ￿ g n )( o , h )=( g 1 ￿ ... ￿ g n )( o , h ) .

Now assume that there is at least one index in K pos .InFigure3weseean
example with two such indexes i and k with i < k . In this case the result of
the multidot expression can be described as either ( g k + 1 ￿ ... ￿ g n )( q , h )

or as

( g i + 1 ￿ ... ￿ g k ￿ g k + 1 ￿ ... ￿ g n )( q , h )

. If we take the greatest index in K pos ,we
get the shortest path to the resulting value and since the rest of the edges are
not affected by the assignment we can describe the result in terms of h .Thisis
expressed in the following properties.

Property 6. ( forall _ K pos ) For all k in K pos ,

( g 1 ￿ ... ￿ g n )( o , h )=( g k + 1 ￿ ... ￿ g n )( q , h )

.

Property 7. ( max _ K pos ) If k = max ( K pos ) ,then

o , h )=(

(

g 1 ￿ ... ￿ g n )( g k + 1 ￿ ... ￿ g n )( q , h

) .