Introduction to the Course (Preface)
Basic Proofs in Separation Logic (Basic)
- A First Taste
- Separation Logic Operators
- Increment of Two References
- Aliased Arguments
- A Function that Takes Two References and Increments One
- Transfer from one Reference to Another
- Specification of Allocation
- Allocation of a Reference with Greater Contents
- The Power of the Frame Rule with Respect to Allocation
- Deallocation in Separation Logic
- Combined Reading and Freeing of a Reference
- Nondeterminism: Specifying Random Output Values
- Recursive Functions
- Summary
- Historical Notes
Representation Predicates (Repr)
- First Pass
- The List Representation Predicate
- Alternative Characterizations of MList
- In-place Concatenation of Two Mutable Lists
- Smart Constructors for Linked Lists
- Copy Function for Lists
- Length Function for Lists
- Alternative Length Function for Lists
- Free Function for Lists
- In-Place Reversal Function for Lists
- More Details
- Optional Material
Heap Predicates (Hprop)
Heap Entailment (Himpl)
Structural Reasoning Rules (Triples)
Reasoning Rules for Term Constructs (Rules)
Semantics of Weakest Preconditions (WPsem)
Weakest Precondition Generator (WPgen)
- First Pass
- More Details
- Definition of wpgen for Each Term Construct
- Computing with wpgen
- Optimizing the Readability of wpgen Output
- Extension of wpgen to Handle Structural Rules
- Lemmas for Handling wpgen Goals
- An Example Proof
- Making Proof Scripts More Concise
- Automated Introductions using the xapp Tactic.
- Database of Specification Lemmas for the xapp Tactic.
- Demo of a Practical Proof using x-Tactics.
- Optional Material
Soundness of the Weakest Precondition Generator (WPsound)
The Magic Wand and Other Operators (Wand)
Affine Separation Logic (Affine)
- First Pass
- Motivation for the Discard Rule
- Statement of the Discard Rule
- Fine-grained Control on Collectable Predicates
- Definition and Properties of heap_affine
- Definition of the "Affine Top" Heap Predicates
- Properties of the \GC Predicate
- Instantiation of heap_affine for a Fully Affine Logic
- Instantiation of heap_affine for a Fully Linear Logic
- Refined Definition of Separation Logic Triples
- Soundness of the Existing Rules
- Soundness of the Discard Rules
- Combined Structural Rules
- More Details
- Optional Material
Reasoning about Arrays (Arrays)
Reasoning about Records (Records)
- First Pass
- Optional Material
- Implementation of Record Accesses using Pointer Arithmetic
- Specification of Record Accesses w.r.t. hfields
- Specification of Record Accesses w.r.t. hrecord
- Implementation of Record Allocation without Initialization
- Implementation of Record Allocation with Initialization
- Extending xapp to Support Record Access Operations