Why Loops End in Cpp
Talkat CppCon 2023 · on Tuesday, 2023-10-03· at 15:15· Cottonwood 2/3, 6700 North Gaylord Rockies Boulevard·
summary
A concrete scheme shows how to encode why a loop ends directly in lightly extended C++ by adding function interfaces with pre/postconditions that record stability, substitutability, repetition and small axioms for primitives. A simple verifier (robot) checks those properties; examples include counting across digit widths, handling base‑10 edge cases (need a special case at 10) and using static_asserts to supply missing facts (e.g. 12) so the verifier can prove termination. The approach composes and works on the presented examples.
AI-written summary · about
chapters (22)
- 0:00Loop termination in C++
- 2:12Heat death of the universe
- 4:42Local reasons for termination
- 6:30Robot-friendly interfaces
- 12:08Analyzing simple loops
- 14:45Proving trivial termination
- 15:48Counting loops and proofs
- 18:39Edge cases in termination
- 21:34Static assertions in proofs
- 22:16Loop variants and ordinals
- 28:02Variants as resources
- 29:05Resource exhaustion in loops
- 31:15Variants without counters
- 33:03Counting theorem implementation
- 37:24Integer breakdown for proofs
- 44:52Bitless integer termination
- 46:38Unsigned bit integer proofs
- 49:47Signed bit integer proofs
- 50:07Multi-bit integer proofs
- 54:48Refactoring to postconditions
- 59:31Generalizing termination proofs
- 1:00:13Summary
related talks
01h 54mCan C++ be 10x Simpler & Safer?
01h 00mDefensive Programming Done Right, Part I
53mInvestigating C++ Legacy Design Trends: Newer Isn’t Always Better!
01h 00mC++11/14 at Scale: What Have We Learned?
01h 30mContracts, Safety, and the Art of Cat Herding
56mThe art of keeping your project from falling apart
01h 03mKeynote: Abstraction Patterns
39mFireside Chat