一句话：提出延迟绑定抽象语法，将属性重化为数据结构并与测试执行器解耦，实现可编程的属性测试语言。
基于属性的测试（PBT）中，用户编写可执行规约即属性，由框架反复检查。现有框架通常把属性写在浅嵌入 DSL 中，属性定义与测试方式紧耦合，用户只能使用框架作者预先提供的配置，若需更多灵活性往往要重写框架。本文提出一种更深层的属性语言，基于混合嵌入的“延迟绑定抽象语法”（deferred binding abstract syntax），将属性具体化为数据结构，与执行属性的 property runner 解耦。作者分别在 Rocq 与 Racket 中实现该语言，利用依赖类型与动态类型的能力，并快速原型化多种 property runner，展示可编程测试带来的领域特定测试改进。
Property-based testing (PBT) is a popular technique for establishing confidence in software, where users write properties---i.e. executable specifications--that can be checked many times in a loop by a testing framework. In modern PBT frameworks, properties are usually written in shallowly embedded domain-specific languages, and their definition is tightly coupled to the way they are tested. Such frameworks often provide convenient configuration options to customize aspects of the testing process, but users are limited to precisely what library authors had the prescience to allow for when developing the framework; if they want more flexibility, they may need to write a new framework from scratch. We propose a new, deeper language for properties based on a mixed embedding that we call deferred binding abstract syntax, which reifies properties as a data structure and decouples them from the property runners that execute them. We implement this language in Rocq and Racket, leveraging the power of dependent and dynamic types, respectively. Finally, we showcase the flexibility of this new approach by rapidly prototyping a variety of property runners, highlighting domain-specific testing improvements that can be unlocked by more programmable testing.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2602-18545,
title = {Programmable Property-Based Testing},
author = {Alperen Keles and Justine Frank and Ceren Mert and Harrison Goldstein and Leonidas Lampropoulos},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {ICFP},
year = {2026},
doi = {10.1145/3828685}
}