Book contents
- Frontmatter
- Dedication
- Contents
- Road map
- Acknowledgments
- 1 Introduction
- I Generic separation logic
- 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
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
- 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
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.
- Type
- Chapter
- Information
- Publisher: Cambridge University PressPrint publication year: 2014