3

我正在创建一个用于学习目的的图形框架。我正在使用 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);
}

好的，真棒，它的工作原理。这里只有一个症结，我已经证明这些功能只适用于这种情况。然而，在我的图论课程中，我所做的只是在数学上证明定理（归纳、矛盾等）。

所以我想知道有没有一种方法可以在数学上证明我的单元测试的正确性？那么有没有一个好的做法呢。因此，我们正在测试该单元的正确性，而不是针对某个特定结果对其进行测试。

4

6 回答 6

5

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

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

但是，您可以通过结合单元测试和代码覆盖率来发现这个错误。然而，即使有 100% 的代码覆盖率，也可能存在任何测试都没有发现的逻辑错误。

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

于 2011-03-04T07:17:07.357 回答
2

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

  • 在实现行为之前，您可以通过编写测试来验证您的测试是否有效。
  • 然后您会看到测试失败。
  • 然后，您实现行为以通过该测试，并且仅通过该测试。永远不要编写不需要实现测试的代码。
于 2011-03-04T07:17:11.147 回答
1

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

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

如果你想对你的东西进行正式证明，总有Coq、Agda和类似的语言，但是写单元测试太费劲了 :)

对测试与证明的一个伟大而简单的介绍是简而言之 Patrick Cousot中的抽象解释。

于 2011-03-04T07:22:31.590 回答
0

我的 2 美分。这样看：你认为你写了一个做某事的函数，但你真正做的是写一个你认为它做某事的函数。如果您无法为代码的功能编写数学证明，您也可以将函数视为假设；你不能确定它总是正确的，但至少它是可证伪的。

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

于 2012-06-22T17:27:44.700 回答
0

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

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

NASA 有一个专门研究形式化方法的部门。

于 2011-03-04T07:23:32.053 回答
0

如果您想检查代码的正确性，您可以如前文所述，应用一些形式验证工具。这不是一件容易的事，但可能仍然可行。有像Key 系统这样的工具能够证明 Java 代码的一阶属性。Key 在泛型、浮点数和并行性等方面存在一些问题，但对于 Java 语言的大多数概念都非常有效。此外，您可以根据证明树自动创建带有 Key 的测试用例。

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

于 2014-01-30T08:36:23.987 回答