2

Haskell 有一个很好的特性，即一段代码的类型签名有时会告诉你该代码做了什么。这让我开始思考……你能根据类型签名构建测试吗？

例如，考虑一个模块，例如Data.Map. 它定义了一个数据类型和几个对该类型进行操作的函数。只看类型签名，应该有可能[原则上]找出所有可能的构造Map值的方法。我的意思是在算法上是可能的——应该可以编写一些程序来获取模块的接口，并计算出你可以针对它进行的所有可能的函数调用。

现在，有些人认为编写良好的测试套件可以看作是库应该做什么的“规范” 。显然，编写代码的人知道他们想要做什么，而机器不知道。但是，鉴于您提供的类型签名，机器应该能够计算出可能要求的内容。

作为更具体的情况，假设有一些不变量应该适用于所有可能的Map值。（例如，，null m == (size m == 0)或者内部健全性检查函数应该始终返回 true。）可以想象编写一个测试框架，将模块交给它，然后说“类型的值Map X Y应该始终满足这些不变量”，然后让测试框架开始尝试执行您提供的功能的所有可能组合以生成地图并检查它们是否满足所有条件。如果没有，它会告诉您违反了什么条件以及构造此无效值所需的表达式。

我的问题是，这种方法听起来容易处理吗？可取的？有趣的？你会如何解决这样的问题？Djinn 似乎已经知道如何在给定预先存在的函数和常量的情况下构造指定类型的值，因此尝试提出具有给定类型的多个表达式听起来并不难。什么样的启发式方法可以用来尝试获得良好的代码覆盖率？（显然，分析代码而不仅仅是类型要困难得多......赖斯定理潜伏在等待中。）

（请注意，我并不是建议这种机器检查应该取代手写测试代码。这个想法更多是为了增强它；也许在更困难的情况下，机器可以咳出可能的表达，然后问人类什么“正确”的答案应该是。然后可以将其记录为新的测试用例，以便在测试套件运行时运行。）

4

3 回答 3

3

您现在可以使用的最接近的东西可能是 QuickCheck 或 SmallCheck——“基于属性”的测试库。

类似 QuickCheck 的测试的典型示例是reverse

>>> quickCheck $ \s -> s == reverse (reverse s)
True

QuickCheck 使用类型类机制来创建Arbitrary各种类型的随机（称为）示例，然后检查这些随机实例的属性。正确选择Arbitrary的实例Map可以在创建您正在寻找的测试类型方面有所帮助。

这里有更多的选择。如果你检查一些依赖类型的语言，比如 Idris 和 Agda，你可以在一个强大得多的类型系统上获得“受 Haskell 影响的”语法，该类型系统能够静态地证明程序的属性。这与 QuickCheck 相去甚远（它已经与单元测试相去甚远），因为它不再依赖于创建合适的Arbitrary实例以适当地捕获感兴趣的问题空间的能力。

除了完全依赖类型的语言之外，您可能对使用Liquid Haskell证明可能的某些类型感兴趣。

于 2013-10-28T20:12:07.487 回答
1

扩展“aavogt”的评论：

Irulan 采用一组标识符，构造涉及这些标识符的所有可能的类型良好的表达式，并搜索在执行时抛出异常的表达式。

如果一个函数抛出一个异常，当然这不一定是一个错误；很可能存在您期望抛出异常的表达式。但 Irulan 会找到所有这些并将它们展示给您，因此您可以决定哪些是合法的，哪些是错误的。

似乎 Irulan 不会发现任何不会导致异常的错误。（特别是，应该抛出异常但不会被发现的表达式。）不会捕获非终止或不正确的结果，也不会捕获过多的资源使用。（话又说回来，机器如何自动找出“正确”的结果应该是什么？心灵感应？）

我觉得有趣的是测试数据生成的方法。Irulan 查找类型的值构造函数，或者如果它们不在范围内，则尝试查找产生适当类型值的函数。它根本不使用Eq实例，而是更喜欢使用 case-blocks（或投影函数，如果它无法获取构造函数）来检查值。

循环的事情是 Irulan 如何使用懒惰的技巧来懒惰地生成测试数据。例如，如果您正在尝试测试该函数，那么列表中实际包含哪些数据length并不重要，只关心列表有多大。Irulan 可以自动计算出来，因此它会生成几种不同大小的列表，但它不会费心将任何数据放入列表中。像 QuickCheck 这样的框架会毫无用处地生成数百个列表大小相同但内容不同的测试用例。

例如，Irulan 可以生成一个包含三个“洞”的列表。如果您触摸其中一个孔，则会引发异常。但是，孔是编号的，例外情况是其中有孔号。Irulan 捕捉到异常，因此“知道”您触摸了哪个洞。然后，它可以系统地用每个可能的类型良好的值替换那个洞（它本身又递归地用洞填充）。在这种方法中，搜索树被修剪为仅对实际测试中的代码重要的部分。

我没有意识到异常和惰性以这种方式相互作用，以允许人们“观察”原本不透明代码的内部操作。我觉得这真的很有趣...

我还应该指出，Irulan 博士论文包含对与该问题相关的其他工作的非常详尽的调查。

于 2013-11-26T13:35:50.847 回答
0

扩展Thomas DuBuisson的评论：

你给 QuickSpec 一组值（通常是函数值），它 [理论上] 使用这些值构造所有可能的类型良好的表达式，并尝试找到始终成立的等式。（值得注意的是，这需要正确实现Eq。）

例如，您可能会给它一些类似empty,insert和deletefrom 的东西Data.Map，并期望得到类似的规则insert x (insert y empty) == insert y (insert x empty)。同样，这只有在Data.Map有一个Eq实例并且它实际上可以正常工作时才能正常工作。

这个想法似乎是，如果您看到弹出的规则显然是虚假的，或者如果您没有看到您希望看到的规则，那么您的代码中可能存在错误。（再说一次，如果您知道您期望什么规则，请首先使用 QuickCheck！）另一种可能性是让 QuickSpec 生成一个规则系统，然后将这些规则转换为 QuickCheck 属性。现在你可以重构你的代码并检查它的可观察行为没有改变。

这是一种有趣的方式来接近这个主题，如果一开始有点奇怪。顺便说一句，我发现 QuickSpec 实际上可以凭空想出一个这样的规则系统，这很有趣。这似乎几乎是神奇的。很酷的东西...

于 2013-11-26T13:23:37.497 回答