Introduction to the Course (Preface)
Basic Proofs in Separation Logic (Basic)
Representation Predicates (Repr)
Heap Predicates (Hprop)
Heap Entailment (Himpl)
Reasoning Rules (Rules)
Semantics of Weakest Preconditions (WPsem)
- First Pass
- More Details
- Optional Material
- A Concrete Definition for Weakest Precondition
- Equivalence Between all Definitions Of wp
- An Alternative Definition for Weakest Precondition
- Extraction Rule for Existentials
- Combined Structural Rule
- Alternative Statement of the Rule for Conditionals
- Definition of wp Directly from hoare
- Historical Notes
Weakest Precondition Generator (WPgen)
- First Pass
- More Details
- Definition of wpgen for Term Rules
- 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
- Further Improvements to the xapp Tactic.
- Demo of a Practical Proof using x-Tactics.
- Optional Material
The Magic Wand Operator (Wand)
- First Pass
- Intuition for the Magic Wand
- Definition of the Magic Wand
- Characteristic Property of the Magic Wand
- Magic Wand for Postconditions
- Frame Expressed with hwand: the Ramified Frame Rule
- Ramified Frame Rule in Weakest-Precondition Style
- Automation with xsimpl for hwand Expressions
- Evaluation of wpgen Recursively in Locally Defined Functions
- More Details
- Optional Material
- Equivalence Between Alternative Definitions of the Magic Wand
- Operator hforall
- Alternative Definition of qwand
- Equivalence between Alternative Definitions of the Magic Wand
- Simplified Definition of mkstruct
- Texan Triples
- Direct Proof of wp_ramified Directly from Hoare Triples
- Conjunction and Disjunction Operators on hprop
- Summary of All Separation Logic Operators
- Historical Notes
Affine Separation Logic (Affine)
- First Pass
- Motivation for the Discard Rule
- Statement of the Discard Rule
- Fine-grained Control on Collectable Predicates
- Definition of heap_affine and of haffine
- 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
- Discard Rules in WP Style
- Exploiting the Discard Rule in Proofs
- Example Proof Involving Discarded Heap Predicates
- More Details
- Optional Material
Arrays and Records (Struct)
- First Pass
- Representation of a Set of Consecutive Cells
- Representation of an Array with a Block Header
- Specification of Allocation
- Specification of the Deallocation
- Specification of Array Operations
- Representation of Individual Records Fields
- Representation of Records
- Example with Mutable Linked Lists
- Reading in Record Fields
- Writing in Record Fields
- Allocation of Records
- Deallocation of Records
- Combined Record Allocation and Initialization
- More Details
- Optional Material
- Refined Source Language
- Realization of hheader
- Introduction and Elimination Lemmas for hcells and harray
- Proving the Specification of Allocation and Deallocation
- Splitting Lemmas for hcells
- Specification of Pointer Arithmetic
- Specification of the length Operation to Read the Header
- Encoding of Array Operations using Pointer Arithmetic
- Encoding of Record Operations using Pointer Arithmetic
- Specification of Record Operations w.r.t. hfields and hrecord
- Specification of Record Allocation and Deallocation
Assertions, Loops, N-ary Functions (Rich)
- First Pass
- More Details
- Semantics and Basic Evaluation Rules for For-Loops
- Treatment of Generalized Conditionals and Loops in wpgen
- Notation and Tactics for Manipulating While-Loops
- Example of the Application of Frame During Loop Iterations
- Reasoning Rule for Loops in an Affine Logic
- Curried Functions of Several Arguments
- Primitive n-ary Functions
- Optional Material
Triples for Nondeterministic Languages (Nondet)
- First Pass
- More Details
- Optional Material
- Interpretation of evaln w.r.t. eval and terminates
- Small-Step Evaluation Relation
- Small-Step Characterization of evalns: Attempts
- Small-Step Characterization of evaln: A Solution
- Reasoning Rules for evalns
- Triples for Small-Step Semantics
- Reasoning Rules for triplens
- Weakest-Precondition for Small-Step Semantics.
- Equivalence Between Non-Deterministic Small-Step and Big-Step Sem.
- Historical Notes
Triples for Partial Correctness (Partial)
- First Pass
- Optional Material
- Interpretation of evalnp w.r.t. eval and safe
- Small-Step Characterization of Partial Correctness
- Reasoning Rules w.r.t. Small-Step Characterization
- Small-Step Characterization of Divergence
- Coinductive, Small-Step Characterization of Partial Correctness
- Equivalence Between the Two Small-Step Charact. of Partial Correctness
- Equivalence Between Small-Step and Big-Step Partial Correctness Semantics
- Historical Notes