Test Driven Development vs Automated Theorem Proving

Question

One thing I've come to be interested in in digital logic/architecture design is Automated Theorem Proving to verify, for example, a floating point multiplication module.

Unit tests are handy, but its almost intractable to try to test (brute-force) every possible input to a floating-point module. Instead, you find either a proof for (1) that it will always generate a correct result or (2) a proof that shows it will generate at least one incorrect result.

I'm trying now to integrate similar logic into my software, and I'm wondering if I could use it either in conjunction with Test Driven Development or in place of Test Driven Development?

Answer 1

In the past I have had quite a lot of experience with formal verification, although it was for hardware components (VHDL/Verilog). The same principles could be applied to software, but if you have any kind of I/O or events, the input space becomes unmanageable. It is also impractical to prove any kind of statement on a large "model" as the state-space becomes too large.

Ideally, you would use a theorem prover on "computational" functions to prove their correctness. However, testing should still be used for several reasons:

• There might be "bugs" in your theorem. This is especially "dangerous" if the person writing the theorems is the person writing the actual code being tested.
• The theorems being tested are often not complete.
• You must place assertions in your test environment to make sure the assumptions you used for the inputs ("environment") of your code are valid.