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

error. If K pos is empty then the multidot expression is unchanged. Otherwise, let
k be the greatest element in K pos . The result is then as stated in max _ K pos (with a
shift of indexes due to lists starting at 0 in PVS). But again because e ￿ Current
is not equal to e when evaluated on void, we have to make a special case for
when the multidot expression ends exactly at e . There is a similar lemma that
combines empty _ K pre and min _ K pre .
The intuitive way to prove these properties is by induction on gs .Thein-
tention is to reason about the last edge of the multidot expression and use the
inductive hypothesis on the path that leads to it. The problem with this ap-
proach is that on the non-empty case we have to reason about a list of the form
cons ( g , gs )

. Therefore, we get to reason about the first edge, not the last one.
To overcome this problem we defined a function multidot _ rev that chains the
arguments in the reverse order. Then we wrote lemmas that are adapted to work
with the reversed list, and we proved them by induction on gs . Finally, the orig-
inal lemmas were proven using their reversed counterpart by instantiating gs
with reverse ( gs ) .

5 Linearised Abstractions

In this section we look at examples of abstract models expressed in terms of
multidot field expressions. We call this style of specifying linearised , because it
is not by recursion on the structure of the abstract model. The properties derived
in the previous section provide us a set of tools to reason about the effects of an
assignment to a linearised abstraction.

5.1 Paths

The following definition abstracts a path embedded in the heap to a list l of
Object s. The i th object in l is the object on the heap that can be accessed by
requesting the first i fields describing the path.
Path ( gs : list [ Name ], l : list [ Object ])
( o:Object v ⊥ , h:Heap ⊥ ) : bool =
length ( gs ) + 1

= length ( l ) ∧

∀ ( i : below [ length ( l )]) :

multidot ( take ( gs , i ))( o , h )

= nth ( l , i )
Due to the possibility of undefinedness, we define the abstractions as predicates
about the heap and the current object rather than as functions because in PVS
functions must be total.
With the use of the spatial separation lemmas for multidot expressions we can
prove the following separation lemma for paths (recall that h =( f := q )( p , h ) ):

Property 8. If for all i < length ( l ) it holds that p = nth ( l , i ) or f = nth ( gs , i ) ,

and ¬ bottom? ( f ( p , h )) ,then

Path ( gs , l )( o , h )=

(

gs , l

)(

o , h

) .

Path