
Specification can not be proven correct, code can.

Posted: Jul 28, 2006 5:56 AM


> Is there truly such thing as provably correct code? Even > though some code can be proven to be correct with regards > to a specific specification, what guarantees that > specification to be correct? The solution and the > challenge go on ad infinitum without resolution. > <p> > On the other hand code can be viewed as always correct, if > you take it to be its own specification. > <p> > How do you like them apples?
Specification can not be proven correct, code can.
First of all, code IS specification. It is just that code is a lower level specification than specs.
In order to prove code correct, you have to check it against specification. If it conforms to all the constraints of the specs, then it is correct.
But how can you prove the specs correct? you need another set of specs, that are even higher level, to prove the initial specs correct.
And then how do you prove the higher level specs correct? you need an even more higher level specs.
The conclusion is: for each level of specification S, you need another level of specification S' that proves S correct.
This means that code can only be proven relatively correct, unless there is a specification U that is provable by itself; that would be the ultimate specification (thus the U term). Then the code would be absolutely correct.

