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

that says whether by traversing bt in the order specified by path , we arrive at
v . Basically get _ node maps each constructor application to the corresponding
field name. We can now describe a binary tree on the heap by mapping each of
its nodes to a multidot field access:

binary_tree_abstraction ( bt : binary_tree [ Object ])
( o:Object v ⊥ , h:Heap ⊥ ) : bool =

∀ ( x : Object , path : list [ Name ]) :

get_node ( bt , path , x )

⇒

= x
From the properties about multidot expressions presented in Section 4 one can
obtain separation and interference lemmas for binary trees.
The same ideas can be applied to other tree-like structures. First make a
linearised abstraction of the data structure: obtain the path from the root to each
of its elements and use that path to describe the pointer structure in terms of
multidot expressions. Then use the properties of Section 4 when reasoning about
assignments. Data structures with loops can also be specified, e.g., a circular list
is just a path that starts and ends in the same object.

multidot ( path )( o , h )

6 Evaluation and Future Work

A natural way to define abstractions is by means of recursion on the structure
of the abstract model. We single out the work by Mehta and Nipkow that uses
this approach to verify several pointer programs [11]. The advantage of using
induction is that it is a familiar general-purpose method that is integrated in the
theorem prover. Much work has been devoted to automate proofs by induction, in
particular to heuristics to instantiate the inductive hypothesis, e.g. rippling [4]. In
the inductive approach one still has to reason about the effect of the assignments
to the data structure, whereas using the rules given in Section 4 the focus is on
when to apply each rule and in finding the extrema of the K -sets, which requires
an instantiation.
Our experience is that both approaches require a comparable amount of proof
work. However, there is still work to be done on investigating specialised version
of the assignment rules and on the integration with the theorem prover as tactics.
For example, if we know that there is no loop on a multidot expression, as is the
case in tree-like structures, then we also know that the K -sets are either empty
or have only one element. This eliminates the need to find the minima or the
maxima.
Because both approaches lead to definitions that are essentially equivalent,
the same properties hold. Hence, our approach can be seen as a complement
rather than a replacement of inductive reasoning.
Reasoning about assignments ultimately reduces to reasoning about object
equality. Therefore, this framework would benefit from knowledge about the
layout of the memory. The separation rules are used to provide local reasoning,
but they are not a primitive of the logic as the star conjunct is in Separation