This blog post (20 minutes read) shows that program correctness is a difficult subject. We will see that sometimes it is ‘easy to ask’ but ‘difficult to deliver’. The entire blog post is summarized by these two slogans:
To show a program is correct, requires one to find an invariant. To show there is no correct program, also requires one to find an invariant.
Correctness is impossible to attain if the requirements are inconsistent.
Extensive analysis of a problem is required to obtain (1) a formal description of the problem, and (2) proof that the requirements are consistent. Even before one starts writing a program, one already has to face a difficult problem: namely, to check that the requirements are consistent! This blog post shows a concrete example that consistency is not always the case—even when the problem looks simple. If we then have requirements that are satisfiable, we then face the second difficult problem: does there exist a correct program at all? The blog post also shows that, no, this is not obvious either. To show that a non-trivial program (i.e. involving a loop) is correct, we face a difficult problem: it requires us to come up with an invariant. On the other hand, to show that there does not exist a correct program at all, we also need to formulate an invariant that any program preserves but which the final required state violates.
Enjoy!
Back to top