clojure.spec.alpha 验证正确性推理过程是怎样的？

Question

你好！
我正在研究 clojure.spec.alpha 的一个实现，并发现了一些相当“小”的测试集（根据我的朴素预期）：）

Clojure spec 定义了一组基本构造函数，这些构造函数可以相互组合。
换句话说，Clojure spec 定义了一种语言来描述结构及其预测性质。

假设 spec 的语义在 原理 和 指南 中非正式描述，那么你是如何推理声明语义与 spec 实现之间的对应关系的呢？

我原先预期有一个包含基本场景和大范围组合（类似于归纳基础）的庞大测试集。如果归纳基础是正确的，那么其他组合也应该是好的。

你是如何推理 clojure.spec.alpha 验证实现正确性的呢？

更新：根据 Alex Miller 首次回答，把问题语境缩小到了 验证 方面。

Answer 1

你主要是在询问验证、兼容性、描述还是生成方面的问题吗？

Comments

让我们将“验证”定义为一种主要上下文

---

验证的基础层是基于谓词的，大量重用了Clojure中的谓词。这些谓词本身大致简单且由定义保证正确（因为它们与Clojure本身使用的同类谓词相同）。例如，字符串通过string?检查，该检查确保对象是java.lang.String的实例。因此在spec中并没有太多这种类型的测试 - 我们利用了一个工作良好的基础。

对于构建，通常每个结构不会有太多的案例，但https://github.com/clojure/spec.alpha/blob/master/src/test/clojure/clojure/test_clojure/spec.clj正在测试原语组合来覆盖它们。当然，做得更多会更好，但我们真的希望在生成测试规范和值方面花些时间（但这在没有spec的情况下很难实现！）。

---

当然，做更多会更好，但最终还是希望花些时间在生成用于测试的规范和值（但这在没有规范的情况下有点棘手）。

通过某种方式生成规范，然后通过生成的规范生成器生成值，并通过生成的规范验证值，这合理吗？
因此，通过使用生成的规范生成器解决了值生成问题，这无疑将耦合引入整个生成器逻辑层，因此验证责任未被单独测试。