Recursive Assertions for Data Structures
Joxan Jaffar, Andrew E. Santosa R · 2007
We present an assertion language for expressing properties of data structures. Its key features are constraints over arrays, multisets and integers which allow the specification of basic assertio ns, and rules, which allow the recursive specification of assertions. Thi s language can thus be used to define assertions to an arbitrary level of expressiveness, ranging from low-level properties of memory allocation, for example, to abstract properties of complex data structures such as AVL trees. The main result is a proof method for verification conditions arising from a program annotated with assertions. The method has two main components. First and foremost is an unfolding algorithm which works by reducing the recursive definitions so that a co n- straint proof may now be applied. Here we introduce a notion of coinduction which forms the basis for termination of the unfold- ing process. The second step is to reduce the constraints, which in general contain expressions involving all the three data ty pes of in- tegers, arrays and multisets, into a base constraint involv ing only integer constraints. Base constraints can then be dispense d with available solvers. We finally show via a small benchmark of classic examples that our proof method is practical. (Copyright notice will appear here once 'preprint' option i s removed.) on the structure of another pointer q. Conversely, there is also need to consider explicit aliasing information. For example, if q points to the third cell of an acyclic list p, and if a three-step traversal of p results in r, we would require that q = r. The most important challenge of all, however, is to capture abstract properties of data structures in such a way that the formal techniques are in tandem with the intuitive reasoning embodied in the user program. In this paper, we address these issues, amongst others, by fir st defining a language of array, multiset and integer expressio ns. The class of integer expressions includes both array elements and ar- ray indices. These basic formulas can describe basic and detailed properties about mutable heaps and pointers. We then embed this formalism in Constraint Logic Programming (CLP) so that CLP predicates can be used to describe recursive properties of data struc- tures. This formulation of recursion then provides for the s pecifica- tion of basic closure properties, amongst other properties . Further, because the CLP formalism has a well-understood logical reading, assertion predicates can be designed to represent abstract proper- ties of data structures. At the same time, low-level specific ations, such as pointer arithmetic or memory management operations, can be represented by the rich constraint language. In particul ar, our formalism supports a notion of separation (19) by simply using multiset constraints to specify that certain heaps do not in tersect. The main contribution is a proof method for CLP assertion pred- icates. We present an algorithm which is based on a standard notion of unfolding definitions. The main novelty is the use of left and right unfolding, augmented with a principle of coinduction which forms the basis for terminating the unfolding process. This unfold- ing process ultimately reduces the proof obligation to another that no longer contains (recursive) assertion predicates. That is, what remains is to prove a constraint. The secondary contribution is an algorithm for proving a con- straint. The algorithm reduces the proof of a constraint involving array, multiset and integer constraints, into a proof invol ving only integer constraints. The novelty in our approach is in how the ar- ray and multiset constraints are arithmetized, that is, con verted into equivalent integer constraints. At this point, the remaini ng proof obligation can be dispensed with standard constraint solvers. We finally argue, via examples, that our proof methodology is intuitive and expressive, and amenable to a practical implementa- tion. We show via a small benchmark of classic examples that our automatic proof method is in fact practical.