让 Property-Based Testing 变得可编程
Programmable Property-Based Testing
传统的 Property-Based Testing (PBT) 框架虽然流行，但用户往往受限于库作者预设的配置选项，难以灵活定制测试逻辑。本文提出了一种基于“延迟绑定抽象语法”的深层嵌入语言，将测试属性重构为数据结构，从而彻底解耦属性定义与执行器。该方案在 Rocq 和 Racket 中实现，利用依赖类型和动态类型的优势，让开发者能够像搭积木一样快速原型化各种专用的 Property Runner，解锁了以往难以实现的领域特定测试优化能力。
我们提出了一种新的、更深层的属性语言，基于一种我们称之为延迟绑定抽象语法的混合嵌入，它将属性具体化为数据结构，并将其与执行它们的属性运行器解耦。