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

modelling idea of Burstall [5]. Refinements of this modelling have been used
as the core of weakest pre-condition calculus-based tools such as Krakatoa for
the verification of Java programs, and Caduceus for the verification of C pro-
grams [7,10]. A separation analysis tailored to integration with the component-
as-array modelling has been proposed by Hubert and Marché [9]. Future work
on the integration of this analysis with our work has been discussed in Section 6.
A well-studied approach to obtain local reasoning is that of Separation Logic,
proposed by Reynolds [14], which can be seen as a radical refinement of Burstall's
idea. In Separation Logic disjointness of portions of the heap is made explicit
in the logic. Its frame rule allows one to reason about just the relevant portion
of the heap that a piece of code manipulates and later augment it with the rest
of the heap. So far, no concrete case studies on industrial software make use of
Separation Logic, but there is ongoing research on its automation, see e.g. [6,1].
An implementation of [1] has been developed inside the theorem prover HOL by
Tuerk [17].
A related line of research is Region Logic, whose goal it is to preserve the
local reasoning of Separation Logic, but without using non-standard semantics
of Hoare-triples. See [15] for recent work.

8 Conclusions

In this paper we have presented a novel approach to reason about assignments
in recursive data structures. We have shown how recursive pointer structures
can be described in terms of paths obtained by a series of field accesses. We
have provided a formal model of these paths as multidot expressions and we
have proved a set of rules that describe how an assignment can affect them.
Using these rules we have derived separation and interference lemmas for lists
and verified an in-place list reversal algorithm. A complete formalisation of the
presented work has been carried out in the PVS theorem prover. We have also
shown how to apply this approach to reason about other data structures and we
have compared it with the standard inductive approach.

Acknowledgments. The authors would like to thank Marko van Eekelen and
Sjaak Smetsers for their insightful comments on a draft version of this paper and
the anonymous reviewers for their comments.

References

1. Berdine, J., Calcagno, C., O'Hearn, P.: Smallfoot: Modular automatic asser-
tion checking with separation logic. In: de Boer, F., Bonsangue, M., Graf, S.,
de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115-137. Springer,
Heidelberg (2006)
2. Blanco, J., Pablo, C.: A semantics for proving class correctness (2005)

(unpublished)