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 和测试值的测试上（但这是没有 spec 的事情很棘手！）。

---

当然，做更多会更好，但最终希望在生成测试规格和值方面投入一些时间（但如果没有规格，这会很困难）

是否可以这样做：以某种方式生成规格，然后通过生成的规格生成器生成值，并通过生成的规格来验证值？
因此，通过使用生成的规格生成器解决了值生成的问题，这无疑给整个生成器逻辑层带来了耦合，验证责任也无法孤立地测试。