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

Thinking again in terms of graphs, this lemma says that if an edge outside the
path is modified, then the path is not affected by the assignment. To give an
idea of how the multidot rules are applied, we sketch the proof of this lemma.

Proof sketch. We are supposed to show that the Path predicates are logically
equivalent. In expanded form, we have to show that the following predicates are
equivalent:

∀ ( i 1 : below [ length ( l )]) : ( g 1 ￿ ... ￿ g i 1 )( o , h )= nth ( l , i 1 ) (2)

∀ ( i 2 : below [ length ( l )]) : ( g 1 ￿ ... ￿ g i 2 )( o , h )= nth ( l , i 2 ) (3)

To show that (2) implies (3), we instantiate i 1 with i 2 and we apply empty _ K pos .
Then we have to show that K pos is indeed empty. If this was not the case then

there would be a k such that

p =( g 1 ￿ ... ￿ g i k )( o , h )= nth ( l , k )

and f = g k ,

which is a contradicts the assumption that p is not in l . For the converse direc-
tion, we apply empty _ K pre in an analogous way.

The interference property for paths describes how a path ending in p can be
joined with a path beginning at q :

Property 9. If p / ∈ l 0 ++ ++

l 1 and c

= (

l 0 ++

) ,then

q car p

Path ( gs 1 ++ f ++ gs 2 , l 0 ++ p ++ q ++ l 1 )( c , h )

=

( Path ( gs 1 , l 0 ++ p )( c , h ) ∧

Path ( gs 2 , q ++ l 1 )( q , h ))

The proof uses the multidot rules empty _ K pos and max _ K pos for the implication
from left to right and it uses the rules empty _ K pre and min _ K pre from right to
left. We omit the proof sketch of this property for reasons of space.
An important point about the proofs using linearised abstractions is that the
induction is encapsulated in the rules about multidot expressions; to prove the
above properties, we did not apply induction.

5.2 Example: Verification of an In-Place List Reversal Algorithm

The Path abstraction can be specialised by Path ( g , l ) , which instantiates the

regular Path with a list of g -fields. By requiring the last node of Path ( next , l )
to point to void, we obtain an abstraction for lists on the heap:

List ( l : list [ Object ])
( o:Object v ⊥ , h:Heap ⊥ ) : bool =
Path ( next , l )( o , h )

∧
IF cons? ( l ) THEN void? ( next ( last ( l ), h ))
ELSE void? ( o )