QuickSpec: A Lightweight Theory Exploration Tool (...)
summary
QuickSpec automatically finds equations by random testing for a given Haskell signature (examples: rev (rev xs) ≡ xs, associativity of ++, many zip/rev identities), now extended to conditional equations (e.g. ABS x + ABS y ≡ ABS (x+y) when signs match). It handles polymorphism and higher‑order functions, plugs into Isabelle for generating lemmas, and shows practical limits: term‑size scaling and occasional instantiation bugs that affect what it discovers.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 0:50What is QuickSpec
- 2:25How to use QuickSpec
- 4:35Associativity
- 7:43Zero Dabs
- 9:40Conditionals
- 12:15Lists
- 16:05Bottoms
- 16:40Higherorder functions
- 17:15Fold map fusion
- 19:25How QuickSpec works
- 22:15Lists of functions
- 22:50Finding equivalences
- 27:50Phils laws
- 30:20Wrong clicks
- 33:35Finding equations
related talks
38mLiving with Spec
47mSpecs2, from starters to dessert and... a look in the kitchen.
34mSymbolic Execution for Randomized Programs
28mMaking property based testing easier
15mIronSpec: Increasing the Reliability of Formal Specifications
47mTesting the Hard Stuff and Staying Sane
36mQuickstrom: Specifying and Testing Web Applications
51mWhen Types are Not Enough