# PrefaceIntroduction to the Course

# Welcome

*Software Foundations*series, which presents the mathematical underpinnings of reliable software.

*Software Foundations*, which presents Verifiable C, a program logic and proof system for C. For OCaml programs, this aspect will be covered in a yet-to-be-written volume presenting CFML, a tool that builds upon all the techniques presented in this volume.

*Software Foundations*Volume 1 (

*Logical Foundations*), and the two chapters on Hoare Logic (Hoare and Hoare2) from Software Foundations Volume 2 (

*PL Foundations*). Volume 5 is not a prerequisite. The exposition here is intended for a broad range of readers, from advanced undergraduates to PhD students and researchers.

# Separation Logic

*program logic*: it enables one to establish that a program satisfies its specification. Specifications are expressed using triples of the form {H} t {Q}. Whereas in Hoare logic the precondition H and the postcondition Q describe the whole memory state, in Separation Logic H and Q describe only a fragment of the memory state that includes the resources necessary to the execution of t.

{ H } t { Q } | |

{ H \* H' } t { Q \* H' } |

*separating conjunction*operator of Separation Logic.

- Automated proofs: the user provides only the code, and the tool locates sources of potential bugs. A good automated tool provides feedback that (at least most of time) is relevant.
- Semi-automated proofs: the user provides not just the code, but also specifications and invariants. The tool then leverages automated solvers (e.g., SMT solvers) to discharge proof obligations.
- Interactive proofs: the user provides not just the code and its specifications, but also a detailed proof script justifying the correctness of the code. These proofs may be developed interactively using a proof assistant such as Coq.

# Separation Logic in a Proof Assistant

- higher-order logic provides virtually unlimited expressiveness that enables formulating arbitrarily complex specifications and invariants;
- a proof assistant provides a unified framework to prove both the implementation details of the code and the underlying mathematical results, e.g., results from number theory or graph theory;
- proof scripts may be easily maintained to reflect changes to the source code; and
- the fact that Separation Logic itself is formalized in the proof assistant provides high confidence in the correctness of the tool.

- A formalization of the syntax and semantics of the source language.
This is called a
*deep embedding*of the programming language. - A definition of Separation Logic predicates as predicates in
higher-order logic. This is called a
*shallow embedding*of the program logic. - A definition of Separation Logic triples as a predicate, the statements of the reasoning rules as lemmas, and the proof of these reasoning rules with respect to the semantics.
- An infrastructure that consists of lemmas, tactics and notations, allowing for the verification of concrete programs to be carried out through relatively concise proof scripts.
- Applications of this infrastructure to the verification of concrete programs.

# Multiple Reading Depths

- The
*First Pass*section presents the most important ideas only. The course in designed in such a way that it is possible to read only the*First Pass*section of every chapter. The reader may be interested in going through all these sections to get the big picture, before revisiting each chapter in more detail. - The
*More Details*section presents additional material explaining in more depth the meaning and the consequences of the key results. This section also contains descriptions of the most important proofs. By default, readers would eventually read all this material. - The
*Optional Material*section typically contains the remaining proofs, as well as discussions of alternative definitions. The*Optional Material*sections are all independent from each other. These sections are intended for (1) readers who plan to continue studying Separation Logic beyond the present course, and (2) teachers using the course.

# Overview

*teaching units*: if the chapters were taught as part of a University course, one could reasonably aim to cover one teaching unit per week.

- (1) Basic: introduction to the core features of Separation Logic,
illustrated using short programs manipulating references.
- (1) Repr: introduction to representation predicates in Separation
Logic, in particular for describing mutable lists and trees.
- (2) Hprop: definition of the core operators of Separation Logic.
- (2) Himpl: definition of the entailment relation, statement and
proofs of its fundamental properties, and description of the
simplification tactic for entailment.
- (3) Triples: definition of Separation Logic triples in terms
of the semantics of the programming language.
- (3) Rules: statement and proofs of the reasoning rules of
Separation Logic, and example proofs of programs using these rules.
- (4) Wand: introduction of the magic wand operator and other
Separation Logic operators, and to the ramified frame rule.
- (4) WPsem: definition of the semantic notion of weakest
precondition, and statement of rules in weakest-precondition style.
- (5) WPgen: presentation of a function that effectively computes
the weakest precondition of a term, independently of its
specification.
- (5) WPsound: soundness proof for the weakest precondition
generator; the contents is for the most part optional.
- (6) Affine: description of a generalization of Separation Logic
with affine heap predicates, which are useful, in particular, for
handling garbage-collected programming languages.
- (6) Arrays: specification of both ML-style arrays with headers,
and C-style arrays with pointer arithmetic.
- (6) Records: representation predicate for records, allowing to isolate arbitrary subsets of the record fields.

# Other Distributed Files

- LibSepReference: a long file that defines the program
verification tool that is used in the first two chapters, and whose
implementation is discussed throughout the other chapters. Each
chapter from the course imports this module, as opposed to importing
earlier chapters.
- LibSepVar: a formalization of program variables, together with
a bunch of notations for parsing variables.
- LibSepFmap: a formalization of finite maps, which are used for
representing the memory state.
- LibSepSimpl: a functor that implements a powerful tactic for
automatically simplifying entailments in Separation Logic.
- LibSepMinimal: a minimalistic formalization of a soundness
proof for Separation Logic.
- All other Lib* files are imports from the TLC library, which is described next.

*Programming Language Foundations*).

## System Requirements

## Feedback Welcome

## Exercises

*Logical Foundations*).

*Disclaimer*: the difficulty ratings currently in place are fairly speculative. You feedback is very much welcome.

*Disclaimer*: (for instructors) the auto-grading system has not been tested for this volume. If you are interested in using auto-grading for this volume, please contact the author.

## Recommended Citation Format

@book {Chargueraud:SF

_{6},

author = {Arthur Charguéraud},

editor = {Benjamin C. Pierce},

title = "Separation Logic Foundations",

series = "Software Foundations",

volume = "6",

year = "2024",

publisher = "Electronic textbook",

note = {Version 2.0, \URL{http://softwarefoundations.cis.upenn.edu} },

}

# Thanks

*Software Foundations*series has been supported, in part, by the National Science Foundation under the NSF Expeditions grant 1521523,

*The Science of Deep Specification*.

(* 2024-01-03 14:46 *)