Book contents
- Frontmatter
- Dedication
- Contents
- Road map
- Acknowledgments
- 1 Introduction
- I Generic separation logic
- II Higher order separation logic
- 12 Separation logic as a logic
- 13 From separation algebras to separation logic
- 14 Simplification by rewriting
- 15 Introduction to step-indexing
- 16 Predicate implication and subtyping
- 17 General recursive predicates
- 18 Case study: Separation logic with first-class functions
- 19 Data structures in indirection theory
- 20 Applying higher-order separation logic
- 21 Lifted separation logics
- III Separation logic for CompCert
- IV Operational semantics of CompCert
- V Higher-order semantic models
- VI Semantic model and soundness of Verifiable C
- VII Applications
- Bibliography
- Index
18 - Case study: Separation logic with first-class functions
from II - Higher order separation logic
Published online by Cambridge University Press: 05 August 2014
- Frontmatter
- Dedication
- Contents
- Road map
- Acknowledgments
- 1 Introduction
- I Generic separation logic
- II Higher order separation logic
- 12 Separation logic as a logic
- 13 From separation algebras to separation logic
- 14 Simplification by rewriting
- 15 Introduction to step-indexing
- 16 Predicate implication and subtyping
- 17 General recursive predicates
- 18 Case study: Separation logic with first-class functions
- 19 Data structures in indirection theory
- 20 Applying higher-order separation logic
- 21 Lifted separation logics
- III Separation logic for CompCert
- IV Operational semantics of CompCert
- V Higher-order semantic models
- VI Semantic model and soundness of Verifiable C
- VII Applications
- Bibliography
- Index
Summary
In a conventional separation logic we have a “maps-to” operator a ↦ b saying that the heap contains (exactly) one cell at address a containing value b. This operator in the separation logic corresponds to the load and store operators of the operational semantics.
Now consider two more operators of an operational semantics: function call and function definition. When function names are static and global, we can simply have a global table relating functions to their specifications—where a specification gives the function's precondition and postcondition. But when the address of a function can be kept in a variable, we want local specifications of function-pointer variables, and ideally these local specifications should be as modular as the rest of our separation logic. For example, they should satisfy the frame rule. That is, we might like to write assertions such as (a ↦ b) * (f : {P}{Q}) meaning that a is a memory location containing value b, and a different address f is a function with precondition P and postcondition Q. Furthermore, the separation * guarantees that storing to a will not overwrite the body of f.
To illustrate these ideas in practice, we will consider a tiny programming language called Cont. The functions in this language take parameters f(x, y, z) but they do not return; thus, they are continuations.
- Type
- Chapter
- Information
- Program Logics for Certified Compilers , pp. 111 - 122Publisher: Cambridge University PressPrint publication year: 2014