In building a Hoare logic over a language specified by an operational semantics, we can view the assertions of the Hoare logic as predicates on the states of the operational semantics. But we do this in two layers: first, relate the operational states into semantic worlds; then, apply the Hoare assertions to the worlds. We do this for several reasons: The operational states may contain information that we want to hide from the Hoare assertions, particularly control information (program counter, control stack) that is not supposed to be visible to a Hoare-logic assertion. The semantic worlds may contain information that we want to hide from the operational semantics, such as step-indexes, ghost variables, predicates in the heap (for modeling first-class functions or mutex locks), and permission-shares. For convenience in reasoning, we require Liebniz equality on worlds—equivalent worlds should be equal—but operational states do not generally satisfy Liebniz equality. In our two different toy examples (Chapter 9 and Chapter 39) we have separated operational states from semantic worlds, and we do so for the VST Separation Logic for CompCert C light.

Some components of the world are subject to separating conjunction (*), and others are not. Generally, to “heap” or “memory” or any other addressable component of the world, we apply separation in order to reason about antialiasing. Nonaddressable local variables (and the addresses of addressable local variables) do not require separation, because there is no aliasing to worry about.

Synopsis: Separation logic is a formal system for static reasoning about pointer-manipulating programs. Like Hoare logic, it uses assertions that serve as preconditions and postconditions of commands and functions. Unlike Hoare logic, its assertions model anti-aliasing via the disjointness of memory heaplets. Separation algebras serve as models of separation logic. We can define a calculus of different kinds of separation algebras, and operators on separation algebras. Permission shares allow reasoning about shared ownership of memory and other resources. In a first-order separation logic we can have predicates to describe the contents of memory, anti-aliasing of pointers, and simple (covariant) forms of recursive predicates. A simple case study of straight-line programs serves to illustrate the application of separation logic.

In constructing program logics for particular applications, for particular languages, 20th-century scientists had particular difficulty with pointers—aliasing and antialiasing, updates to state, commuting of operators; and self-reference—recursive functions, recursive types, functions as first-class values, types and predicates as parameters to functions. The combination of these two was particularly difficult: pointers to mutable records that can contain pointers to function-values that operate on mutable records.

Two strains of late-20th-century logic shed light on these matters.

• Girard's 1987 linear logic [43] and other substructural logics treat logical assertions as resources that can be created, consumed and (when necessary) duplicated. This kind of thinking led to the Ishtiaq/O'Hearn/Reynolds invention in 2001 of separation logic [56, 79], which is a substructural Hoare logic for reasoning about sharing and antialiasing in pointer-manipulating programs.

• Scott's 1976 domain theory [84] treats data types as approximations, thereby avoiding paradoxes about recursive types and other recursive definitions/specifications: a type can be defined in terms of more approximate versions of itself, which eventually bottoms out in a type that contains no information at all. These ideas led to the Appel/McAllester/Ahmed invention in 2001 of step-indexing [10, 2] which is a kind of practical domain theory for computations on von Neumann machines.

Many 21st-century scientists have generalized these methods for application to many different program logics (and other applications); and have formalized these methods within mechanical proof assistants.

We illustrate the use of tactical proof (semi)automation on the program shown in Figure 27.1. We compile this source program reverse.c into a C-light abstract-syntax data structure using the front end of CompCert, the clightgen utility. This produces a Coq file reverse.v with a sequence of definitions in the CompCert abstract-syntax tree structures (Figure 27.2).

Clightgen comprises CompCert's (unverified) parser into CompCert C, followed by CompCert's (verified) translation into C light. The fact that one or another of these front-end phases is unverified does not concern us, because we apply the program logic to the output of these translations. If we specify correctness properties of reverse.v and prove them, then the C light program will have those properties, regardless of whether it matches the source program reverse.c. Of course, it is very desirable for reverse.v to match reverse.c, so the programmer may reason informally about unverified properties of reverse.c such as timing, information flow, or resource consumption.

This program uses linked lists of 32-bit integers. Before proceeding with the verification, we should develop the theory of list segments (a “theory” is just what we call a collection of definitions, lemmas, and tactics useful for reasoning about the subject matter). Chapter 19 explained the theory of list segments; in the file list.v we build an lseg theory parameterized by a C structure definition.

Synopsis: In Part III we showed how to apply a program logic interactively to a program, using tactics. Here we will show a different use of program logics: we build automatic static analyses and decision procedures as efficient functional programs, and prove their soundness using the rules of the program logic.

Synopsis: Verifiable C is a style of C programming suited to separation-logic verifications; it is similar to the C light intermediate language of the CompCert compiler. We show the assertion language of separation-logic predicates for specifying states of a C execution. The judgment form semax of the axiomatic semantics relates a C command to its precondition postconditions, and for each kind of command there is an inference rule for proving its semax judgments. We illustrate with the proof of a C program that manipulates linked lists, and we give examples of other programs and how they can be specified in the Verifiable C program logic. Shared-memory concurrent programs with Dijkstra-Hoare synchronization can be verified using the rules of concurrent separation logic.

Synopsis: Instead of reasoning directly on the model (that is, separation algebras), we can treat separation logic as a syntactic formal system, that is, a logic. We can implement proof automation to assist in deriving separationlogic proofs.

Reasoning about recursive functions, recursive types, and recursive predicates can lead to paradox if not done carefully. Step-indexing avoids paradoxes by inducting over the number of remaining program-steps that we care about. Indirection theory is a kind of step-indexing that can serve as models of higher-order Hoare logics. Using indirection theory we can define general (not just covariant) recursive predicates.

Recursive data structures such as lists and trees are easily modeled in indirection theory, but the model is not the same one conventionally used, as it inducts over “age”—the approximation level, the amount of information left in the model—rather than list-length or tree-depth. A tiny pointer/continuation language serves as a case study for separation logic with first-class function-pointers, modeled in indirection theory. The proof of a little program in the case-study language illustrates the application of separation logic with function pointers.