From Formal Specification to Property Based Test
summary
A gem named spec2pbt parses formal specifications and scaffolds runnable Property Based Tests plus a separate config file, lowering only safe, recognized patterns into tests. It finds the FIFO-vs-LIFO bug in a Stack by producing a minimal counterexample and contributes stateful property-based testing upstream to the pbt gem. The analysis uses a pattern catalog of about twenty-something patterns. Current limits: two spec languages partially supported, narrow pattern coverage, and generated tests need improved readability.
AI-written summary · about
chapters (13)
- 0:00Introduction and motivation
- 3:26Why formal methods matter
- 6:02Formal specifications explained
- 8:53Property based testing overview
- 11:48Combining specs and tests
- 12:32Introducing spec2pbt tool
- 16:20Tool design decisions
- 18:12Scaffold vs compiler approach
- 20:20Safe regeneration design
- 21:46Upstream contributions
- 23:36Pattern analysis process
- 26:54Future directions and limits
- 29:06Conclusion and Q&A
related talks
23mFrom test to proof: introduction to Property Based Testing
58mProperty Based Testing: Concepts and Examples
01h 24mIntroduction to Property Based Testing
51mProperty-Based Testing
36mProperty-Based Testing: Unveiling the Truth on Test Reduction
43mProperty-Based Testing - Examples from Business Applications
01h 31mIntroduction to Property-Based Testing
28mMaking property based testing easier