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

Logic [14] (see also Section 7). Hubert and Marché [9] propose a static separation
analysis and show how it can be integrated in the component-as-array modelling.
They split the heap into regions that are inferred by the separation analysis and
accordingly relabel the field names as a combination f _ r of the old field name f
and a region r . This could be integrated into our model, for example by redefining
the heap as
Heap : TYPE =

[ Object → Object v ]]
When it is inferred that two objects x and y lie in separate regions, the com-
parison between them can be avoided and the separation lemmas can be applied
automatically.

[ Region , Name →

7 Related Work

A first version of some of the rules presented in Section 4 first appeared in
Tamalet's Master's thesis [16].
In the seminal work of Bornat [3] and also in the work by Meyer on a semantics
for Eiffel [12], pointer structures on the heap are related with abstract models
via repeated composition of field requests. This has been a source of inspiration
for this paper. Bornat and Meyer both define a sequence closure operator that
repeatedly requests a series of (the same) fields, yielding the list of objects that
is traversed on the heap. This is essentially the same as our Path abstraction of
Section 5.2. In this paper we have given a complete and formalised overview of
the effects of assignments to arbitrary multidot field expressions. A treatment of
the sequential operator in the context of Eiffel has been given in an unpublished
work by Blanco and Castro [2], restricted to the case of lists.
A perhaps more natural way to define abstractions is by the use of recursion on
the structure of the abstract model. Mehta and Nipkow [11] used this approach
to verify the correctness of several pointer programs. We have compared the
inductive approach and the linearised approach in Section 6.
Hoare and Jifeng [8] introduce a framework for the formulation of assertions
about objects and pointers based on trace model of graphs and process algebra.
They use a graphical notation very similar to the one used in this paper. However,
their model uses graph transformations to describe the changes to the state
whereas we use an operational semantics.
Our rules about an assignment followed by a multidot are meta-level proper-
ties of the language. To enable this meta-level reasoning we introduced a function
multidot that maps a list of Name s to a suitable expression, which is essentially
a deep embedding of multidot expressions. The rules about multidot expressions
are a reflection of the properties 1 and 2. For an instructive paper on reflection
with examples in PVS we refer to [18].

Local Reasoning

Local reasoning is the key to scalability in formal verification of programs. The
way the heap is modelled in our framework is based on the component-as-array