TODO: Part IV and V and extra case studies
christetreault opened this issue · 1 comments
christetreault commented
The following sections of the book remain to be written:
Part IV : Abstract Refinements (TODO)
- Abstract Refinements I (code)
- FLOPS/IHP talk sequence
- Vanilla/Code [compose, foldr, ...]
- Abstract Refinements II (data)
- RecRef [List, BST]
- Arrays
- Abstract Refinements III (bounds)
- compose
- filter
- state
Part V: Tips and Tricks (TODO)
- Tips:
- Inductive strengthening
- Materializing Proofs
- Assumes/Dynamic Checking
- Tricks: Totality
- Tricks: Termination
- Copy from BLOG/PAPER sequence
- HW Exercises
Extra Case Studies
-
Case Study 1: AlphaConvert (tests/pos/alphaconvert-List.hs)
-
Case Study 2: Kmeans
-
grep FIXME/TODO (!)
-
move HINT to ABOVE code block
-
Subtyping exercises
- div by zero
- array-bounds
- create (bytestring)
-
LH fix
- allow using CoreToLogic definitions (e.g. member) in
predicates/aliases not just other measures #332
- allow using CoreToLogic definitions (e.g. member) in
-
convert measure refinements into invariants, e.g.
measure size :: [Int] -> Nat
should yield invariant {v:[a] | 0 <= size v}
? Intelligible parse errors
- Web demo
christetreault commented
This issue is being opened per discussion with @ranjitjhala on issue #18