Abstract
In the third lecture, we studied data structures and the verification of programs that manipulate them. Arrays are the oldest of data structures. A simple extension of Hoare's logic with a rule for assignment to an element of an array makes it possible to specify and verify many programs using arrays, such as sort-in-place.
Pointers, also known as references, can be used to represent a wide range of data structures: graphs, chained lists, trees, etc. Encoding pointers in terms of global arrays, as proposed by R. Burstall (1972) and developed by R. Bornat (2000), is effective for verifying algorithms operating on graphs, but very cumbersome for algorithms on lists and other chained structures. Indeed, it is difficult to avoid the sharing, aliasing and interference situations that can invalidate these structures.
It was in an attempt to describe and control these interference phenomena that J. C. Reynolds, later joined by P. O'Hearn and H. Yang, invented the logic of separation between 1997 and 2001. This logic highlights the importance of local reasoning and associated framing rules, the need to associate a memory footprint with each assertion, and the concept of separating conjunctions between assertions.
We have illustrated the approach by developing a separation logic for a small functional and imperative language with immutable variables and pointers to mutable memory locations. This separation logic makes it possible to describe many data structures very precisely using representation predicates: simply or doubly chained lists, circular lists, trees, etc., and to specify and verify their main operations.
Finally, we outline two proofs of the semantic correctness of this separation logic, one based on a property of non-determinism of memory allocation; the other, on quantization over all possible frames.
