7

After some research, I understand that:

Like I see here, a formal proof is just a mathematical calculation, based on a mathematical expression (boolean expression).

A unit test is checked from assertions, so mainly on one or a set of boolean expressions.

Moreover, I read (very quickly) a research's paper of unit test generation from formal proof.

  • Is unit testing a form of formal method (here I think to a system like formal proof)?
  • If it's totally separate concept what are the differences?

The aim of this question is not to know if after running unit testing there still bugs. His aim is to know if there is a link between unit testing and formal method.

csblo
  • 239
  • 3
  • 9
  • 2
    "Formal methods ensures us of the absence of bugs in a program" Citation needed. Seriously, that is such bull. There have been comparison studies around the cost and benefit of various formal and other methods, and none of them are a silver bullet. – l0b0 Apr 10 '15 at 08:42
  • 1
    I don't want a "silver bullet", the aim of this question is not to choose between unit testing and formal proof, I just want to understand. – csblo Apr 10 '15 at 08:50
  • That was an extremely bold claim, without a real reference (you need to link to or at least name the article and section), rather than "ref: Wikipedia". That's like "ref: A book". Hence my rebuttal. – l0b0 Apr 10 '15 at 10:13
  • possible duplicate of [Unit Tests work but there are still bugs?](http://programmers.stackexchange.com/questions/206967/unit-tests-work-but-there-are-still-bugs) – gnat Apr 10 '15 at 10:22
  • 1
    @l0b0 That claim is true. It is not a silver bullet, because it would take massive amount of effort and skill to apply to anything else than trivial case. – Euphoric Apr 10 '15 at 10:44
  • Well, a unit test is a formal proof of the fact that your program obeys a certain correctness property (the assertion) for one specific input. – usr Apr 10 '15 at 11:29
  • 2
    For people looking for the famous [Dijkstra](http://en.wikipedia.org/wiki/Edsger_W._Dijkstra) quotes on this issue, [link 1 (cs.utexas.edu)](http://www.cs.utexas.edu/~EWD/transcriptions/EWD03xx/EWD303.html), [link 2 (en.wikiquote.org)](http://en.wikiquote.org/wiki/Edsger_W._Dijkstra). That said, quotes shouldn't be used in lieu of a proof. – rwong Apr 10 '15 at 12:15
  • @gnat: you know you gave a link to a question which contains **not one word** (not even in the answers) about formal methods? This is clearly not a dupe. – Doc Brown Apr 10 '15 at 13:40
  • @DocBrown that's because, [as explained in *accepted* answer](http://programmers.stackexchange.com/a/278734/31260), "The two are different things, and in fact much more different in practice than they would be in theory..." – gnat Apr 10 '15 at 13:41
  • 2
    Unit tests test particular inputs; formal methods test all possible inputs at once. – user253751 Apr 10 '15 at 23:45

2 Answers2

28

The two are different things, and in fact much more different in practice than they would be in theory.

A formal correctness proof proves something about the behaviour of an algorithm. For instance, it might investigate the invariants applying to the data as it is transformed by a sorting algorithm, and prove that if the algorithm terminates, every element is larger than the previous one. This kind of proof can be rigorous, i.e. if it's done correctly the algorithm cannot be wrong in this respect.

In practice, algorithms must be embodied in computer code, and it's usually infeasible to prove that a given bit of code accurately represents the algorithm that you want. (That would require formally proving the behaviour of the compiler, the standard library, the virtual machine, etc.) It gets a little easier the more similar the programing language is to the mathematical notation you've used in the formal proof, but not much. (The code running in central systems of the Space Shuttle was said to be almost a perfect mathematical notation itself, but not very pleasant to program in.)

It's much more cost-effective to actually run the code on judiciously chosen inputs and verify that it produces the expected outputs. This has the disadvantage that you can never be certain that there isn't an error in it - it might behave for those input/output pairs you haven't tested (and there are usually more pairs than you can test, or you wouldn't need a computer program to do the work in the first place), or worse, the code might be subtly non-deterministic or context-dependent in way that your tests don't expose.

But in practice, most errors that affect a computation can be exposed with intelligent checks, and if you keep a record of known errors and test cases verifying they cannot recur, the quality of code can generally be made good enough to be of business value. Certainly it's a better idea to run unit tests, integration tests and user acceptance tests and get something out the door that people will pay for than to conduct a lengthy, expensive formal proof that overlooks a subtle deviation between the written specification and the actual expectations of the customer. So in the real world, the two are almost completely distinct activities.

Kilian Foth
  • 107,706
  • 45
  • 295
  • 310
10

There is no precise, universally accepted definition of "formal method". However, most definitions imply some form of mathematical rigour, formalism or proof, none of which a unit test provides.

A unit test is simply "try it out and see if it works in this one single specific case", whereas formal methods try to prove that "it always works in every case under every condition in every environment".

Jörg W Mittag
  • 101,921
  • 24
  • 218
  • 318
  • 2
    I disagree with what formal methods prove. I would say "it always works provided the following clearly specified assumptions holds...". For example when proving behavior in parallel computing you would almost always assume weak fairness on the part of the scheduler, and usually assume strong fairness. – Taemyr Apr 10 '15 at 11:02
  • 1
    Well, the nature of a proof is always that it proves exactly what it states to prove, and nothing more. And it is of course important to take a very hard look at exactly *what* a proof states to prove. For example, in Java, for a method with a return type of `String`, the type checker can prove that *if* the method returns, it will either return with an error, a `String` or `null`, but it cannot prove that the method will return at all, nor can it prove that it won't return anything in addition to the `String` (e.g. a side-effect). – Jörg W Mittag Apr 10 '15 at 11:12