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.
