证明单元测试的正确性

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

好的，真棒它有效。这里只有一个关键，我已经证明这些函数只适用于这种情况。然而，在我的图论课程中，我所做的只是在数学上证明定理（归纳，矛盾等等）。所以我想知道有没有办法证明我的单元测试在数学上是正确的？那么这是一个很好的做法。因此，我们正在测试单元的正确性，而不是针对某个特定结果对其进行测试。

已邀请:

6 个回复

阀傻

不可以。在一般情况下，单元测试并不试图证明其正确性。他们应该测试具体的例子。我们的想法是选择足够的代表性示例，如果出现错误，可能会通过一个或多个测试找到它，但您无法确保以这种方式捕获所有错误。例如，如果您是单元测试添加函数，您可能会测试一些正数，一些是负数，一些是大数，一些是小数，但仅使用这种方法，您很幸运能找到这种实现不起作用的情况：

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

但是，您可以通过组合单元测试和代码覆盖来发现此错误。然而，即使有100％的代码覆盖率，也可能存在任何测试都没有捕获的逻辑错误。可以证明代码的正确性。它被称为形式验证，但它不是单元测试的用途。除了最简单的软件之外，所有这些都很昂贵，因此很少在实践中完成。

丧泉缝锋

可能不是。单元测试通过详尽的测试来解决问题：通过在实现行为之前编写测试来验证测试是否有效。然后你看到测试失败了。然后，您实现行为以传递该测试，并且仅执行该测试。永远不要编写实现测试不需要的代码。

款去芳尾脊

实际上，您所证明的是您的算法的一个案例正在运行，例如您证明您的执行路径的一个子集是有效的。测试永远不会帮助您在严格的数学意义上证明正确性（除了非常简单的情况）。在一般情况下，这是不可能的。测试是解决这个问题的一种实用方法，我们试图表明代表性案例是正确的（边界值，中间某处的值等），并希望这是有效的。仍然，一些工具，如findbugs等，可以为您提供代码某些属性的保守证明。如果你想要你的东西的正式证明，总是有Coq，Agda和类似的语言，但这是一个单独的测试:) 测试与证明之间的一个简单而简单的介绍是Nutshell Patrick Cousot中的抽象解释。

好按紊叉

有正式指定代码操作方式的工具，甚至可以证明它们以这种方式工作的工具，但它们远离单元测试区域。 Java世界中的两个例子是JML和ESC / Java2 NASA有一个专门负责正式方法的部门。

桔适丛

我的2美分。以这种方式看待它：你认为你写了一个能做某事的函数，但你真正做的是编写一个你认为它能做某事的函数。如果你不能写出代码所做的数学证明，你也可以将函数看作假设;你不能确定它总是正确的，但至少它是可以证伪的。这就是为什么我们编写单元测试（注意：只是其他功能，容易出现错误，叹息），试图伪造假设，找到它不具备的反例。

辰炔诚薯

如果您想要获取代码的正确属性，您可以（如前面的帖子中所述）应用一些正式的验证工具。这不是一件容易的事，但可能仍然可行。像KeY系统这样的工具能够证明Java代码的一阶属性。 KeY在泛型，浮点数和并行性等方面存在一些问题，但对于Java语言的大多数概念都很有效。此外，您可以使用基于证明树的KeY自动创建测试用例。如果你熟悉JML（这不是很难学，基本上是带有一些逻辑的Java），你可以尝试这种方法。对于系统中真正关键的部分，验证可能真的需要考虑;对于代码的其他部分，使用单元测试测试一些可能的跟踪可能已经足够，例如为了避免回归问题。

要回复问题请先登录或注册

证明单元测试的正确性

6 个回复

发起人

proof

correctness

问题状态

证明单元测试的正确性

与内容相关的链接

6 个回复

发起人

proof

correctness

问题状态