Though I mean is not to be too formal, it is useful to at least understand the required steps in a formal proof of correctness.
Specifications: Before we prove that an algorithm is correct, we need to know precisely what it is supposed to do.
Preconditions: Assertions that are promised be true about the input instance.
Postconditions: Assertions that must be true about the output.
Correctness: Consider some instance. If this instance meets the preconditions, then after the code has been run, the output must meet the postconditions:
The correctness of an algorithm is only with respect to the stated specifications. It does not guarantee that it will work in situations that are not taken into account by this specification.
Breaking the Computation Path into Fragments: The method to prove that an algorithm is correct is as follows. Assertions are inserted into the code to act as check-points. Each assertion is a statement about the current state of the computation’s data structures that is either true or false. If it is false, then something has gone wrong in the logic of the algorithm. These assertions break the path of the computation into fragments. For each such fragment, we prove that if the assertion at the beginning of the fragment is true and the fragment gets executed, then the assertion at the end of the fragment will be true. Combining all these fragments back together gives that if the first assertion is true and the entire computation is executed, then the last assertion will be true.
A Huge Number of Paths: There are likely an exponential number or even an infinite number of different paths that the computation might take, depending on the input instance and the tests that occur along the way. In contrast, there are not many different computation path fragments. Hence, it is much easier to prove the correctness of each fragment than of each path.
The following table outlines the computational path fragments that need to be tested for different code structures.
