证明单元测试的正确性

Question

我正在创建一个用于学习目的的图形框架。我正在使用 TDD 方法，因此我正在编写大量单元测试。但是，我仍在弄清楚如何证明我的单元测试的正确性

例如，我有这个类（不包括实现，并且我已经简化了它）

public class SimpleGraph(){
 //Returns true on success
 public boolean addEdge(Vertex v1, Vertex v2) { ... }

 //Returns true on sucess
 public boolean addVertex(Vertex v1) { ... }
}

我还创建了这个单元测试

@Test
public void SimpleGraph_addVertex_noSelfLoopsAllowed(){
 SimpleGraph g = new SimpleGraph();
 Vertex v1 = new Vertex('Vertex 1');
 actual = g.addVertex(v1);
 boolean expected = false;
 boolean actual = g.addEdge(v1,v1);
 Assert.assertEquals(expected,actual);
}

好吧，太棒了，它可以工作。这里只有一个症结，我已经证明这些函数只适用于这种情况。然而，在我的图论课程中，我所做的只是用数学方法证明定理（归纳、矛盾等）。

所以我想知道是否有一种方法可以从数学上证明我的单元测试的正确性？那么这方面有没有好的做法呢？因此，我们正在测试该单元的正确性，而不是测试它的某个结果。

Answer 1

不。单元测试不会尝试证明一般情况下的正确性。他们应该测试具体示例。这个想法是选择足够多的代表性示例，如果存在错误，一个或多个测试可能会发现它，但您不能确保以这种方式捕获所有错误。例如，如果您对 add 函数进行单元测试，您可能会测试一些正数、一些负数、一些大数和一些小数，但单独使用这种方法，您会很幸运地发现此实现不起作用的情况

int add(int a, int b) {
    if (a == 1234567 && b == 2461357) { return 42; }
    return a + b;
}

：但是，可以通过结合单元测试和代码覆盖率来发现此错误。然而，即使代码覆盖率达到 100%，也可能存在任何测试未能发现的逻辑错误。

证明代码的正确性是可能的。它被称为形式验证，但这不是单元测试的用途。除了最简单的软件之外，其他软件的执行成本也很高，因此在实践中很少这样做。

Answer 2

可能 不是。单元测试通过详尽的测试来解决问题：

• 您可以通过在实现行为之前编写测试来验证测试是否有效。
• 然后您会看到测试失败。
• 然后，您实现行为来通过该测试，并且仅通过该测试。切勿编写实现测试不需要的代码。

Answer 3

实际上，您要证明的是您的算法的一种情况正在工作，例如您正在证明执行路径的子集是有效的。测试永远不会帮助您证明严格数学意义上的正确性（除了非常简单的情况）。在一般情况下，这是不可能的。测试是解决这个问题的一种务实方法，我们试图证明代表性案例是正确的（边界值、中间某处的值等），并希望它能起作用。

尽管如此，一些工具（例如 findbugs 等）仍设法为您提供代码某些属性的保守证明。

如果您想要正式证明您的东西，总有 Coq、Agda 和类似的语言，但这对于编写单元测试来说是一个巨大的延伸:)

一个关于测试与测试的简单而伟大的介绍校样是摘要解读Patrick Cousot。

Answer 4

有一些工具可以正式指定代码的运行方式，甚至还有一些工具可以证明它们以这种方式工作，但它们距离单元测试领域很远。

Java 世界中的两个示例是 JML 和 ESC/Java2

NASA 有 整个部门致力于正式方法。

Answer 5

我的2分钱。这样看：您认为您编写了一个执行某些操作的函数，但您真正所做的是编写一个您认为它执行某些操作的函数。如果您无法从数学上证明代码的作用，您也可以将该函数视为假设;你不能确定它总是正确的，但至少它是可证伪的。

这就是为什么我们编写单元测试（注意：只是其他函数，容易出现错误，叹息），试图证伪假设，找到不成立的反例。

Answer 6

如果您想确保代码的正确性，您可以像之前的文章中提到的那样，应用一些形式化验证工具。这不是一件容易做到的事情，但仍然是可行的。有像 Key 系统 这样的工具能够证明 Java 代码的一阶属性。 KeY 在泛型、浮点数和并行性等方面存在一些问题，但对于 Java 语言的大多数概念来说效果很好。此外，您可以根据证明树自动使用KeY创建测试用例。

如果您熟悉 JML（这并不难学，基本上是 Java 加上一点逻辑），您可以尝试这种方法。对于系统中真正关键的部分，验证可能确实是需要考虑的事情；对于代码的其他部分，通过单元测试测试一些可能的跟踪可能已经足够了，例如避免回归问题。