如何推理 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会很难！）。

---

"当然，做更多会更好，但最终我还是想花一些时间在生成测试规格和值上（但这在没有规格的情况下是很有挑战性的！）

通过某种方式生成规格，然后通过生成的规格生成器生成值，并通过生成的规格验证值，这有意义吗？
因此，通过使用生成的规格生成器解决值生成问题，无疑会在整个生成器逻辑层带来耦合，因此验证责任没有独立测试。