Book contents
- Frontmatter
- Dedication
- Contents
- Road map
- Acknowledgments
- 1 Introduction
- I Generic separation logic
- 2 Hoare logic
- 3 Separation logic
- 4 Soundness of Hoare logic
- 5 Mechanized Semantic Library
- 6 Separation algebras
- 7 Operators on separation algebras
- 8 First-order separation logic
- 9 A little case study
- 10 Covariant recursive predicates
- 11 Share accounting
- II Higher order separation logic
- 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
6 - Separation algebras
from I - Generic separation logic
Published online by Cambridge University Press: 05 August 2014
- Frontmatter
- Dedication
- Contents
- Road map
- Acknowledgments
- 1 Introduction
- I Generic separation logic
- 2 Hoare logic
- 3 Separation logic
- 4 Soundness of Hoare logic
- 5 Mechanized Semantic Library
- 6 Separation algebras
- 7 Operators on separation algebras
- 8 First-order separation logic
- 9 A little case study
- 10 Covariant recursive predicates
- 11 Share accounting
- II Higher order separation logic
- 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
Separation logics have assertions—for example P * (x ↦ y) * Q—that describe objects in some underlying model—for example “heaplets”—that separate in some way—such as “the heaplet satisfying P can join with (is disjoint from) the heaplet satisfying x ↦ y.” In this chapter we investigate the objects in the underlying models: what kinds of objects will we have, and what does it mean for them to join?
This study of join relations is the study of separation algebras. Once we know how the underlying objects join, this will explain the meaning of the * operator (and other operators), and will justify the reasoning rules for these operators.
In a typical separation logic, the state has a stack ρ for local variables and a heap m for pointers and arrays. Typically, m is a partial function from addresses to values. The key idea in separation logic is that that each assertion characterizes the domain of this function as well as the value of the function. The separating conjunction P * Q requires that P and Q operate on subheaps with disjoint domains.
In contrast, for the stack we do not often worry about separation: we may assume that both P and Q operate on the entirety of the stack ρ.
For now, let us ignore stacks ρ, and let us assume that assertions P are just predicates on heaps, so m ⊨ P is simply P(m).
- Type
- Chapter
- Information
- Program Logics for Certified Compilers , pp. 35 - 43Publisher: Cambridge University PressPrint publication year: 2014