How do you prove a function works?

Question

I've recently gotten the testing religion and have started primarily with unit testing. I code unit tests which illustrate that a function works under certain cases, specifically using the exact inputs I'm using. I may do a number of unit tests to exercise the function. Still, I haven't actually proved anything other than the function does what I expect it to do under the scenarios I've tested. There may be other inputs and scenarios I haven't thought of and thinking of edge cases is expensive, particularly on the margins.

This is all not very satisfying to do me. When I start to think of having to come up with tests to satisfy branch and path coverage and then integration testing, the prospective permutations can become a little maddening.

So, my question is, how can one prove (in the same vein of proving a theorem in mathematics) that a function works (and, in a perfect world, compose these 'proofs' into a proof that a system works)?

Is there a certain area of testing that covers an approach where you seek to prove a system works by proving that all of its functions work? Does anybody outside of academia bother with an approach like this? Are there tools and techniques to help?

I realize that my use of the word 'work' is not precise. I guess I mean that a function works when it does what some spec (written or implied) states that it should do and does nothing other than that.

Note, I'm not a mathematician, just a programmer.

Answer 1

In academica, there is a concept similar to induction in mathematics, it's called structural induction. However, it only applies to functional programming languages and methods with no side effects at all. In others, it is very hard, if not impossible, to prove that a method works due to side effects.

In TDD, you try to formulate edge cases which a method has to fulfill to be valid, however, it is possible to miss such a case. Even if a (non-trivial) method fulfills all your tests, there can be a combination of arguments or a sequence of events you simply didn't think of which will break your code. Simply put: That's life. You can possibly predict all outcomes in a non-trivial implementation, but you can assure that the method works for specific edge cases, expect for some cases that are so edgy you will cut yourself upon touching them. (zing, bad pun).

Answer 2

It sounds like you are defining work as a function doing what you want it to do. Or in other words, you want to prove that you typed out the logic correctly.

Well, in this case, at least assuming a near infinite amount of valid input for a function, you can't really prove something is correct, you can only disprove it. So the idea is to create good unit tests that span the various outputs of the function. It doesn't prove something correct, but can be used to prove something is correct enough.

Answer 3

"It sounds like you are defining work as a function doing what you want it to do" Usually you'll also want to verify a function doesn't do what you didn't want it to do, the definitions are close but not the same, for example an ADD() function can return the correct answer but also print out some extra debugging garbage.

Answer 4

The way to prove that something works, can be done by means of formal proofs. Some techniques are fairly well known, at least in academia. One that comes to mind is "Proof by induction". However, this approach is rather manual, and also fairly error prone to mere mortals, if not simply way too complex.

A different more manageable approach to formal verification is known as "Model Checking". With this approach you express your software in a suitable manner, that allows you to perform certain checks on it (with a tool). One such check could be to check for dead/live-locks in multithreaded applications. Other kinds of checks you can perform, is to make sure that your application will at all times allow the same kinds of interactions as a simpler model of the same application, thereby bringing down the chances of having made the same mistake in both the model and the real application. A tool for model checking could be Spin, but there are many out there.

It seems that Wikipedia has an article on this subject too: Formal Verification