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
15 - Introduction to step-indexing
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
Many kinds of recursive definitions and recursive predicates appear in the descriptions of programs and programming languages. Some recursive definitions, such as list and tree data structures, are naturally covariant; these are straightforward to handle using a simple least-fixed-point method as described in Chapter 10. But some useful kinds of self-referencing definitions are not covariant. When the recursion goes through function arguments, it may be contravariant (see Ffunopt on page 64) or some mixture that is neither covariant nor contravariant. This kind of recursion requires more difficult mathematics, yet it is essential in reasoning about certain kinds of programs:
• Object-oriented programs in which class C has methods with a “this” or “self” parameter of type C;
• Functional programming languages with mutable references at higher types—such as ML;
• Concurrent languages with dynamically creatable locks whose resource invariants can describe other locks—a typical idiom in Pthreads concurrency;
• Functional languages (such as ML) where datatype recursion can go through function-parameters.
Does the C programming language have these features? Well, yes. C's type system is rather loose (with casts to void* and back). C programs that use void* in design patterns similar to objects or function closures can be perfectly correct, but proving their correctness in a program logic may need noncovariant recursion.
This chapter, and the next two chapters (predicate implication and subtyping; general recursive predicates) present the logical machinery to reason about such recursions in the VST program logics.
- Type
- Chapter
- Information
- Program Logics for Certified Compilers , pp. 94 - 98Publisher: Cambridge University PressPrint publication year: 2014