关于 clojure.spec.alpha 验证正确性是如何推理的？

Question

你好！
我正在探索 clojure.spec.alpha 的一个 实现，并发现了一系列相对“小”的 测试 :)

Clojure spec 定义了一组可以相互组合的基本类型。
换句话说，Clojure spec 定义了一种描述结构及其预测性属性的语言。

假设 spec 语义在 动机 和 指南 中非正式描述，您是如何推理声明语义与 spec 实现之间的一致性的呢？

我 expected 一个庞大的测试集合，涵盖了基本场景及其有限数量的组合 -- 类似于归纳基础。如果归纳基础是正确的，那么其他组合也是最有效的。

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

更新：根据 Alex Miller 的第一个回答，将问题背景缩小到 验证 方面。

Answer 1

您主要是在询问验证、一致性、描述或生成吗？

Comments

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

---

验证的基础层是基于谓词的，并且大量使用了Clojure中的谓词。这些谓词本身在很大程度上是简单的，并且根据定义是正确的（因为它们与Clojure自己使用的谓词相同）。例如，通过字符串?检查字符串，以检查对象是否是java.lang.String的实例。因此，spec中不会有很多这样的测试 - 我们利用现有的工作基础。

对于构建，每个构造通常没有太多的案例，但https://github.com/clojure/spec.alpha/blob/master/src/test/clojure/clojure/test_clojure/spec.clj正在测试原语组合来覆盖它们。当然，做得更多会更好，但最终确实想花些时间在生成spec和测试值上（但这是没有spec的棘手问题！）

---

"当然，做更多会更好，但最终确实想花些时间在生成spec和测试值上（但这是没有spec的棘手问题！）"

通过某种方式生成规范后，通过生成的规范生成值，然后通过生成的规范验证值，这样做有意义吗？
因此，通过使用生成的规范生成器解决了值生成的难题，当然这也在整个生成器逻辑层带来了耦合，因此验证责任没有单独进行测试。