>>17
See this is where it gets way off track. When I mentioned provers, I was talking about the coverage angle. If your spec is wrong, if your unit tests are wrong or if you're simply off your meds that day and regression testing last month's code then it's all the same: you've fucked up somewhere and the results are nigh worthless.
The utility of the prover with respect to coverage is that you end up having to write/perform a lot fewer tests.
another assumption is that specifications need to be as precise as the program is. this is not so. code contains a lot of redundancy of expression and information and little expression of intent and purpose. specifications should contain what the code does not.
With respect to this discussion (ca. my post), this is the best passage from that link. A simple specified requirement can set the prover about quite a large amount of code, if it is all involved in producing the result. If that result is the only requirement of that code, a very simple specification can be used to prove a (relatively) very complex portion of the program, and more importantly it gives you coverage even if the spec is wrong. You will know your components work as understood according to specifications even if not as intended by the client. (This might seem useless, but imagine it isn't true: now it's wrong
and broken.)