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.

翻译：基于属性的测试（Property-based testing, PBT）是一种建立软件信心的流行技术，用户编写属性（即可执行的规约），测试框架可以多次循环检查这些属性。在现代PBT框架中，属性通常以浅层嵌入的领域特定语言编写，其定义与测试方式紧密耦合。这类框架通常提供便捷的配置选项以定制测试过程的各个方面，但用户仅限于库作者在开发框架时有先见之明所允许的范围；若需要更大的灵活性，则可能需要从头编写新的框架。我们提出了一种基于混合嵌入的新型深层属性语言，称之为延迟绑定抽象语法，它将属性具体化为数据结构，并将其与执行属性的属性运行器解耦。我们分别在Rocq和Racket中实现了该语言，分别利用了依赖类型和动态类型的能力。最后，我们通过快速原型化多种属性运行器，展示了这种新方法的灵活性，突显了通过更可编程的测试所能实现的领域特定测试改进。