Is “Unit testing” a form of formal method?

Question

After some research, I understand that:

• Formal method contribute to the reliability and robustness of a design. (ref : Wikipedia - Formal method)
• Unit testing ensures us of the absence of errors introduced by a developer (ref : Wikipedia - Unit testing)

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.

Answer 1

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.

Answer 2

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".