patternMajor
Program Correctness, The specification
Viewed 0 times
specificationcorrectnessprogramthe
Problem
From Wikipedia: In theoretical computer science, correctness of an algorithm is asserted when it is said that the algorithm is correct with respect to a specification.
But the problem is that to get the "appropriate" specification is not a trivial task, and there is no 100% correct method (as far as i know) to get the right one, it just an estimation, so if we are going to take a predicate as a specification just because it "looks" like the "one", why not taking the program as correct just because it "looks" correct?
But the problem is that to get the "appropriate" specification is not a trivial task, and there is no 100% correct method (as far as i know) to get the right one, it just an estimation, so if we are going to take a predicate as a specification just because it "looks" like the "one", why not taking the program as correct just because it "looks" correct?
Solution
First off, you're absolutely right: you're on to a real concern. Formal verification transfers the problem of confidence in program correctness to the problem of confidence in specification correctness, so it is not a silver bullet.
There are several reasons why this process can still be useful, though.
-
Specifications are often simpler than the code itself. For instance, consider the problem of sorting an array of integers. There are fairly sophisticated sorting algorithms that do clever things to improve performance. But the specification is fairly simple to state: the output must be in increasing order, and must be a permutation of the input. Thus, it is arguably easier to gain confidence in the correctness of the specification than in the correctness of the code itself.
-
There is no single point of failure. Suppose you have one person write down a specification, and another person write the source code, and then formally verify that the code meets the spec. Then any undetected flaw would have to be present in both the spec and the code. In some cases, for some types of flaws, this feels less likely: it's less likely that you'd overlook the flaw when inspecting the spec and overlook the flaw when inspecting the source code. Not all, but some.
-
Partial specs can be vastly simpler than the code. For instance, consider the requirement that the program is free of buffer overrun vulnerabilities. Or, the requirement that there are no array index out-of-bounds errors. This is a simple spec that is fairly obviously a good and useful thing to be able to prove. Now you can try to use formal methods to prove that the entire program meets this spec. That might be a fairly involved task, but if you are successful, you gain increased confidence in the program.
-
Specs might change less frequently than code. Without formal methods, each time we update the source code, we have to manually check that the update won't introduce any bugs or flaws. Formal methods can potentially reduce this burden: suppose the spec doesn't change, so that software updates involve only changes to the code and not changes to the spec. Then for each update, you are relieved of the burden to check whether the spec is still correct (it hasn't changed, so there's no risk new bugs have been introduced in the spec) and of the burden to check whether the code is still correct (the program verifier checks that for you). You still need to check that the original spec is correct, but then you don't need to keep checking it each time a developer commits a new patch/update/change. This can potentially reduce the burden of checking correctness as code is maintained and evolves.
Finally, remember that specs typically are declarative and can't necessarily be executed nor compiled directly to code. For instance, consider sorting again: the spec says that the output is increasing and is a permutation of the input, but there is no obvious way to "execute" this spec directly and no obvious way for a compiler to automatically compile it to code. So just taking the spec as correct and executing it often isn't an option.
Nonetheless, the bottom line remains the same: formal methods are not a panacea. They simply transfer the (very hard) problem of confidence in code correctness to the (merely hard) problem of confidence in spec correctness. Bugs in the spec are a real risk, they are common, and they can't be overlooked. Indeed, the formal methods community sometimes separates the problem into two pieces: verification is about ensuring the code meets the spec; validation is about ensuring the spec is correct (meets our needs).
You might also enjoy Formal program verification in practice and Why aren't we researching more towards compile time guarantees? for more perspectives with some bearing on this.
There are several reasons why this process can still be useful, though.
-
Specifications are often simpler than the code itself. For instance, consider the problem of sorting an array of integers. There are fairly sophisticated sorting algorithms that do clever things to improve performance. But the specification is fairly simple to state: the output must be in increasing order, and must be a permutation of the input. Thus, it is arguably easier to gain confidence in the correctness of the specification than in the correctness of the code itself.
-
There is no single point of failure. Suppose you have one person write down a specification, and another person write the source code, and then formally verify that the code meets the spec. Then any undetected flaw would have to be present in both the spec and the code. In some cases, for some types of flaws, this feels less likely: it's less likely that you'd overlook the flaw when inspecting the spec and overlook the flaw when inspecting the source code. Not all, but some.
-
Partial specs can be vastly simpler than the code. For instance, consider the requirement that the program is free of buffer overrun vulnerabilities. Or, the requirement that there are no array index out-of-bounds errors. This is a simple spec that is fairly obviously a good and useful thing to be able to prove. Now you can try to use formal methods to prove that the entire program meets this spec. That might be a fairly involved task, but if you are successful, you gain increased confidence in the program.
-
Specs might change less frequently than code. Without formal methods, each time we update the source code, we have to manually check that the update won't introduce any bugs or flaws. Formal methods can potentially reduce this burden: suppose the spec doesn't change, so that software updates involve only changes to the code and not changes to the spec. Then for each update, you are relieved of the burden to check whether the spec is still correct (it hasn't changed, so there's no risk new bugs have been introduced in the spec) and of the burden to check whether the code is still correct (the program verifier checks that for you). You still need to check that the original spec is correct, but then you don't need to keep checking it each time a developer commits a new patch/update/change. This can potentially reduce the burden of checking correctness as code is maintained and evolves.
Finally, remember that specs typically are declarative and can't necessarily be executed nor compiled directly to code. For instance, consider sorting again: the spec says that the output is increasing and is a permutation of the input, but there is no obvious way to "execute" this spec directly and no obvious way for a compiler to automatically compile it to code. So just taking the spec as correct and executing it often isn't an option.
Nonetheless, the bottom line remains the same: formal methods are not a panacea. They simply transfer the (very hard) problem of confidence in code correctness to the (merely hard) problem of confidence in spec correctness. Bugs in the spec are a real risk, they are common, and they can't be overlooked. Indeed, the formal methods community sometimes separates the problem into two pieces: verification is about ensuring the code meets the spec; validation is about ensuring the spec is correct (meets our needs).
You might also enjoy Formal program verification in practice and Why aren't we researching more towards compile time guarantees? for more perspectives with some bearing on this.
Context
StackExchange Computer Science Q#70044, answer score: 30
Revisions (0)
No revisions yet.