Volume 4: QuickChick: Property-Based Testing in Coq
Table of Contents
Index
Preface
Setup
Practicalities
Recommended Citation Format
Thanks
Introduction
A First Taste of Testing
Overview
A Tutorial on Typeclasses in Coq (
Typeclasses
)
Basics
Classes and Instances
Parameterized Instances: New Typeclasses from Old
Class Hierarchies
How It Works
Implicit Generalization
Records are Products
Typeclasses are Records
Inferring Instances
Typeclasses and Proofs
Propositional Typeclass Members
Substructures
Some Useful Typeclasses
Dec
Monad
Others
Controlling Instantiation
"Defaulting"
Manipulating the Hint Database
Debugging
Instantiation Failures
Nontermination
Alternative Structuring Mechanisms
Advice from Experts
Matthieu Sozeau
John Wiegley
Michael Soegtrop
Abhishek Anand
Further Reading
Core QuickChick (
QC
)
Generators
The
G
Monad
Primitive generators
Lists
Custom Generators
Checkers
Shrinking
Exercise: Ternary Trees
Putting it all Together
Sized Generators
Automation
Collecting Statistics
Dealing with Preconditions
Another Precondition: Binary Search Trees
Case Study: a Typed Imperative Language (
TImp
)
Identifiers, Types and Contexts
Identifiers
Types
List-Based Maps
Deciding
bound_to
(optional)
Contexts
Expressions
Typed Expressions
Generating Typed Expressions
Values and States
Values
States
Evaluation
Shrinking for Expressions
Back to Soundness
Well-Typed Programs
Decidable instance for well-typed.
Automation (Revisited)
(More) Typeclasses for Generation
Using "SuchThat" Typeclasses
Acknowledgements
The QuickChick Command-Line Tool (
QuickChickTool
)
Overview
Arithmetic Expressions
QuickChick Test Annotations
Sections
Mutation Testing
A Low-Level Stack Machine
QuickChick Command-Line Tool Flags
QuickChick Reference Manual (
QuickChickInterface
)
The
Show
Typeclass
Generators
Fundamental Types
Structural Combinators
Basic Generator Combinators
Choosing from Intervals
The
Gen
and
GenSized
Typeclasses
Generators for Data Satisfying Inductive Predicates
Shrinking
The
Shrink
Typeclass
The
Arbitrary
Typeclass
The Generator Typeclass Hierarchy
Checkers
Basic Definitions
Checker Combinators
Decidability
The
Dec
Typeclass
The
Dec_Eq
Typeclass
Automatic Instance Derivation
Top-level Commands and Settings
The
quickChick
Command-Line Tool
Test Annotations
Mutant Annotations
Section Annotations
Command-Line Tool Flags
Postscript
Future Directions
Recommended Reading
Bibliography (
Bib
)
