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
- Optional Material
- 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)
The Magic Wand and Other Operators (Wand)
- First Pass
- Definition of the Operator hforall
- Definition of the Operator hor
- Definition of the Operator hand
- Definition of the Magic Wand Operator: hwand
- Definition of the Magic Wand Operator for Postconditions: qwand
- Simplifications of Magic Wands using xsimpl
- Summary of All the Separation Logic Operators
- The Ramified Frame Rule
- More Details
- Optional Material
Semantics of Weakest Preconditions (WPsem)
Weakest Precondition Generator (WPgen)
Soundness of the Weakest Precondition Generator (WPsound)
- More Details
- Definition of the Predicate formula_sound
- Soundness for the Case of Sequences
- Soundness for the Other Term Constructs
- Soundness of the Predicate Transformer mkstruct
- Lemmas Capturing Properties of Iterated Substitutions
- Main Induction for the Soundness Proof of wpgen
- Statement of Soundness of wpgen for Closed Terms
- Optional Material
Affine Separation Logic (Affine)
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