Search papers, labs, and topics across Lattice.
This paper addresses the limitations of existing property-based testing (PBT) frameworks by providing a formal account of Hedgehog's syntax and semantics, revealing that its distribution semantics is non-compositional. To overcome this challenge, the authors introduce Hedgehog$^\rightarrow$, a restricted version of the language based on arrow calculus, which successfully achieves a compositional distribution semantics. The evaluation demonstrates that Hedgehog$^\rightarrow$ retains expressiveness for practical generators while enabling formal justification for program optimizations.
Hedgehog$^\rightarrow$ not only resolves the compositionality dilemma in property-based testing but also maintains practical expressiveness for generator design.
Property-based testing (PBT) is a powerful technique for software verification that relies on random input generators and "shrinking" processes to find and minimize counterexamples to executable specifications called properties. While optimizing these generators is crucial for testing efficiency, formally justifying such optimizations is currently difficult because existing languages lack a compositional semantics that is coarse-grained enough for high-level reasoning. In this paper, we first provide a formal account of the syntax and semantics of Hedgehog, a popular PBT framework. We demonstrate that Hedgehog's distribution semantics - which models how users typically reason about generators - is non-compositional. Furthermore, we prove that any sound and complete compositional semantics for Hedgehog must necessarily be equivalent to its sampling semantics, which is too fine-grained to justify common program optimizations. To resolve this dilemma, we introduce Hedgehog$^\rightarrow$, a restricted version of the language based on the arrow calculus, and prove that Hedgehog$^\rightarrow$ possesses a compositional distribution semantics. We evaluate Hedgehog$^\rightarrow$ through a Haskell implementation and show that it remains expressive enough to capture generators of practical interest, while providing the formal foundation needed for compositional generator equivalence proofs.
