New Foundations for Separation Logic

This thesis presents new foundations for separation logic, an important field within the formal sciences such as theoretical computer science. Around the turn of the millennium, separation logic was introduced by J.C. Reynolds with the goal to make reasoning, about the correctness of computer programs that work with so-called ‘pointers’, more efficient than earlier formal methods. Reynolds’ method and the other earlier methods are both extensions of the proof system introduced by C.A.R. Hoare for reasoning about the correctness of simple while-programs. The essence of Reynolds’ initial work, which was researched and put into practical use by many other scientists, consists of two extensions of the work initiated by Hoare: the first extension adds to first-order predicate logic two new propositional connectives (the so-called separating conjunction and separating implication); the second extension adds to Hoare’s program logic new proof rules for reasoning about (the primitive operations of) pointer programs. These primitive operations are used for reading memory (‘lookup’), writing memory (‘mutation’), reserving memory (‘allocation’), or freeing memory (‘deallocation’).

The new foundations are presented in two parts. The following paragraphs
summarize the contents of these two parts. The first part contains a model-theoretic and proof-theoretic exploration of the classical interpretation of separation logic, the logic used in Reynolds’ assertion language. This first part proves a result for separation logic, that is as fundamental as the corresponding result by Goedel in first-order logic—the completeness theorem. The second part contains a new interpretation of Reynolds’ program logic, and introduces—for the first time—so-called dynamic separation logic. Dynamic separation logic is an extension of dynamic logic by D. Harel. Using dynamic separation logic, an alternative weakest precondition axiomatization and strongest postcondition axiomatization is given. These alternative axiomatizations, in contrast to earlier axiomatizations of Reynolds’ program logic, do have the property of gracefulness: the earlier axiomatizations of Reynolds’ program logic are not graceful, because they unnecessarily increase the complexity in the use of separating connectives when generating weakest preconditions or strongest postconditions.

Chapter 2 of the first part demonstrates the inadequacy of the standard interpretation of separation logic, because it lacks compactness. This chapter also introduces a new interpretation, called the full interpretation of separation logic, that is based on the possibility of evaluating formulas also with respect to infinite heaps. However, also this full interpretation is inadequate. We continue with a search for necessary and sufficient conditions for embedding the standard interpretation into the full interpretation, and we introduce so-called relational separation logic with the goal to compare separation logic with second-order predicate logic. It is an interesting fact that the full interpretation of separation logic lies close to the standard interpretation of second-order logic: expressivity of a so-called binding operator is sufficient for showing that these two logics coincide.

Chapter 3 of the first part introduces a proof theory with a corresponding new interpretation of separation logic that is based on first-order definable heaps. This new interpretation allows us to show that the resulting proof system is in fact adequate. The proof system is presented as a sequent calculus, but also a second proof system is introduced in the natural deduction style. The sequent calculus is sound and complete with respect to first-order definable heaps. The natural deduction calculus is sound and complete with respect to structures that satisfy a semantic comprehension condition. The second proof system works with more general formulas than what is allowed in separation logic, by introducing a connective that is closely related to the binding operator of the previous chapter.

Chapter 4 of the second part comprises: general interpretations of separation logic, and a class of structures based on so-called memory models. The latter class is used in the proof of soundness and relative completeness of Reynolds’ program logic. We arrive at dynamic separation logic by introducing a program modality in the assertion language. We research an alternative weakest precondition axiomatization and strongest postcondition axiomatization for classical separation logic. This work directly leads us to solving an open problem, where it is the question whether the global axioms can be inferred from the local axioms and the frame rule of Reynolds’ program logic but without additionally using the separating implication connective. Our method is robust, since it can also be applied to obtain a weakest precondition axiomatization and strongest postcondition axiomatization for intuitionistic separation logic (this result is not yet published).

The thesis also includes an extensive appendix with background material, concerning higher-order predicate logic and Hoare’s program logic, that is needed to understand and appreciate the above novel results. The appendix also describes an accompanying Coq formalization of the soundness and completeness of the alternative axiomatizations of Reynolds’ program logic, that aims to increase the trust one may place in the validity of the results.