Among the biggest challenges in property-based testing (PBT) is the constrained random generation problem: given a predicate on program values, randomly sample from the set of all values satisfying that predicate, and only those values. Efficient solutions to this problem are critical, since the executable specifications used by PBT often have preconditions that input values must satisfy in order to be valid test cases, and satisfying values are often sparsely distributed. We propose a novel approach to this problem using ideas from deductive program synthesis. We present a set of synthesis rules, based on a denotational semantics of generators, that give rise to an automatic procedure for synthesizing correct generators. Our system handles recursive predicates by rewriting them as catamorphisms and then matching with appropriate anamorphisms; this is theoretically simpler than other approaches to synthesis for recursive functions, yet still extremely expressive. Our implementation, Palamedes, is an extensible library for the Lean theorem prover. The synthesis algorithm itself is built on standard proof-search tactics, reducing implementation burden and allowing the algorithm to benefit from further advances in Lean proof automation.

翻译：在基于属性的测试（PBT）中，最大的挑战之一是约束随机生成问题：给定关于程序值的谓词，从满足该谓词的所有值中随机采样，且仅对这些值进行采样。该问题的有效解决方案至关重要，因为PBT使用的可执行规格说明通常要求输入值必须满足前置条件才能成为有效测试用例，而满足条件的值往往分布稀疏。我们提出了一种利用演绎程序合成思想的新颖方法解决此问题。我们基于生成器的指称语义提出了一组合成规则，这些规则催生了一种自动合成正确生成器的流程。本系统通过将递归谓词重写为catamorphisms并与适当的anamorphisms匹配来处理递归谓词；这在理论上比其他递归函数合成方法更简单，却仍具有极强的表达能力。我们的实现Palamedes是一个面向Lean定理证明器的可扩展库。该合成算法本身基于标准证明搜索策略构建，既降低了实现负担，又能使算法受益于Lean证明自动化领域的后续进展。