# 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*). The reading of 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 for Sequential Programs*, by Arthur Charguéraud. The long version of this paper is available from: http://www.chargueraud.org/research/2020/seq_seplogic/seq_seplogic.pdf.

*supplemental material*linked near the bottom of that page.

# 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. This fragment 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, 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 worked on 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 form, e.g., results from theory or graph theory;
- proof scripts may be easily maintained to reflect on a change to the source code;
- the fact that Separation Logic 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 from
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 notation, 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.

# Several Possible Depths of Reading

- The short curriculum includes only the 5 first chapters (ranging from chapter Basic to chapter Rules).
- The medium curriculum includes 3 additional chapters (ranging from chapter WPsem to chapter Wand).
- The full curriculum includes 5 more chapters (ranging from chapter Partial to chapter Rich).

- 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 details. - 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. They would typically be of interest to readers who want to understand every detail, readers who are seeking for a deep understanding of a particular notion, and readers who are looking for answers to specific question.

# List of Chapters

*teaching units*: if the chapters were taught as part of a University course, one could presumably 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,
of Hoare triples, and of Separation Logic triples.
- (2) Himpl: definition of the entailment relation, statement and
proofs of its fundamental properties, and description of the
simplification tactic for entailment.
- (3) Rules: statement and proofs of the reasoning rules of
Separation Logic, and example proofs of programs using these rules.
- (4) WPsem: definition of the semantic notion of weakest
precondition, and statement of rules in weakest-precondition style.
- (4) WPgen: presentation of a function that effectively computes
the weakest precondition of a term, independently of its
specification.
- (5) Wand: introduction of the magic wand operator and of the
ramified frame rule, and extension of the weakest-precondition
generator for handling local function definitions.
- (5) Affine: description of a generalization of Separation Logic
with affine heap predicates, which are useful, in particular, for
handling garbage-collected programming languages.
- (6) Struct: specification of array and record operations, and
encoding of these operations using pointer arithmetic.
- (6) Rich: description of the treatment of additional language
constructs, including loops, assertions, and n-ary functions.
- (7) Nondet: definition of triples for non-deterministic
programming languages.
- (7) Partial: definition of triples for partial correctness only, i.e., for not requiring termination proofs.

# 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 the chapters that precedes it.
- 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, corresponding to the definitions and proofs
presented in the ICFP'20 paper mentioned earlier.
- All other Lib* files are imports from the TLC library, which is described next.

*Programming Language Foundations*).

## Feedback Welcome

## Exercises

*Logical Foundations*).

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

*Disclaimer*: 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.

## System Requirements

*Logical Foundations*) describes how to install Coq. The files you are reading have been tested with Coq 8.12.

## Note for CoqIDE Users

*asynchronous*proof mode disabled. To load all the course files in CoqIDE, use the following command line.

coqide -async-proofs off -async-proofs-command-error-resilience off -Q . Basic.v &

## Recommended Citation Format

@book {Charguéraud:SF6,

author = {Arthur Charguéraud},

title = "Separation Logic Foundations",

series = "Software Foundations",

volume = "6",

year = "2021",

publisher = "Electronic textbook",

note = {Version 1.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*.

(* 2021-01-27 11:54 *)