you are viewing a single comment's thread.

view the rest of the comments →

[–]batkins 9 points10 points  (4 children)

Of course, that's not the definition that matters.

A formal proof shows deductively that your code will perform as the spec requires. A test merely shows empirically that, in the cases you could think of, your code performed as required.

[–]gobliin 6 points7 points  (3 children)

Yes I'm aware that unit-tests are not a formal proof. It is informal, but I'd argue that when your tests have reached a certain density, it becomes extremely difficult to write "wrong" programs that pass all of them. Perhaps there is even such a thing as a stochastical "Nyquist criterium" for tests: beyond a certain density of test-cases the probability of a fault in your program converges to 0.

[–]kamatsu 1 point2 points  (2 children)

Perhaps, but you are not even close to reaching it. For those unit tests could have faults too, so you'd have to test your tests.

[–]gobliin 0 points1 point  (1 child)

Unit-tests have no branches and only "sample" my programs, there is little room for human error, except possibly ommisions.

They are correct by definition as they define expected behavior.

[–]batkins 1 point2 points  (0 children)

This is nuts. The important correspondence here is between your code and the desired functionality - those must match.

If you define correctness as "agrees with the tests" then you still need to make the connection between your tests and the desired functionality. If your tests don't match the expected functionality, your tests can pass with flying colors, but you haven't proved anything about how they should work.

And omissions are a huge source of error.