Prove correctness of unit test

Question

I'm creating a graph framework for learning purposes. I'm using a TDD approach, so I'm writing a lot of unit tests. However, I'm still figuring out how to prove the correctness of my unit tests

For example, I have this class (not including the implementation, and I have simplified it)

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

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

I also have created this unit tests

@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);
}

Okay, awesome it works. There is only one crux here, I have proved that the functions work for this case only. However, in my graph theory courses, all I'm doing is proving theorems mathematically (induction, contradiction etc. etc.).

So I was wondering is there a way I can prove my unit tests mathematically for correctness? So is there a good practice for this. So we're testing the unit for correctness, instead of testing it for one certain outcome.

Answer 1

No. Unit tests don't attempt to prove correctness in the general case. They should test specific examples. The idea is to pick enough representative examples that if there is an error it will probably be found by one or more of the tests, but you can't be sure to catch all errors this way. For example if you were unit testing an add function you might test some positive numbers, some negative, some large numbers and some small, but using this approach alone you'd be lucky to find the case where this implementation doesn't work:

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

You would however be able to spot this error by combining unit testing and code coverage. However even with 100% code coverage there can be logical errors which didn't get caught by any tests.

It is possible to prove code for correctness. It is called formal verification, but it's not what unit tests are for. It's also expensive to do for all but the most simple software so it is rarely done in practice.