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

Reasoning about Assignments
in Recursive Data Structures

Alejandro Tamalet and Ken Madlener

Institute for Computing and Information Sciences (iCIS),
Radboud University Nijmegen, The Netherlands
{a.tamalet,k.madlener}@cs.ru.nl

Abstract. This paper presents a framework to reason about the effects
of assignments in recursive data structures. We define an operational
semantics for a core language based on Meyer's ideas for a semantics
for the object-oriented language Eiffel. A series of field accesses, e.g.
f 1 ￿ f 2 ￿ ... ￿ f n , can be seen as a path on the heap. We provide rules
that describe how these multidot expressions are affected by an assign-
ment. Using multidot expressions to construct an abstraction of a list,
we show the correctness of a list reversal algorithm. This approach does
not require induction and the reasoning about the assignments is encap-
sulated in the mentioned rules. We also discuss how to use this approach
when working with other data structures and how it compares to the
inductive approach. The framework, rules and examples have been for-
malised and proven correct using the PVS proof assistant.

1 Introduction

In order to verify pointer programs that manipulate recursive data structures,
one generally identifies the pointer structure embedded in the heap with an
abstract model. A concrete instance is a mapping of a set of objects on the heap
connected by a field such as next to an abstract list of objects. The mapping
is called the abstraction and the abstract list is called the abstract model .An
operation performed by the program on a pointer structure on the heap has
a corresponding operation on the abstract model. For example, the operations
performed by a list reversal algorithm have the combined effect that the abstract
list is reversed at the end of the execution. The standard way to define data
abstractions is by recursion on the structure of (the data type of) the abstract
model.
Verification of pointer programs is a non-trivial task due to the possibility
of aliasing. Modifying data through one name implicitly modifies the values
associated to all aliased names. If two portions of the heap are disjoint, an
assignment in one part of the heap does not affect the other; this is called local
reasoning . Local reasoning is essential for scalability and several approaches to
obtain it have been studied, see e.g. Separation Logic [14] and Region Logic [15].
When it is not known how the heap is partitioned or when working within
a region that may contain aliases, we have to reason about how a change to