Correctness of Algorithms PDF

## 8. Correctness ### 8.1 Fundamentals of Correctness In this chapter we would like to discuss how we can be sure, that our algorithms do precisely what they are supposed to do. The correctness of algorithms plays a key role for example in information security, algorithmics and software developmen...

## 8. Correctness ### 8.1 Fundamentals of Correctness In this chapter we would like to discuss how we can be sure, that our algorithms do precisely what they are supposed to do. The correctness of algorithms plays a key role for example in information security, algorithmics and software development. But what does it mean for an algorithm to be correct, since at the least end, an algorithm is just a sequence of statements. The most important part is the specification. It defines the precondition, result, and effect. An algorithm (or in our case a Python/Scala-function) is correct, if for all inputs satisfying the precondition, the algorithm applied to these inputs have the defined result and effect. Hence, when talking about the correctness of an algorithm/function, we already have a useful specification. Here, we have an example for a useless specification: ```python # Precondition: None # Effect: Something is printed on the screen # Result: Something is returned def foo(): print("Hallo") return 42 ``` Although the given function precisely fulfils the specification, it is useless, because the specification does not give us enough information. A useful specification would be: ```python # Precondition: None # Effect: "Hallo" is printed on the screen # Result: 42 is returned def foo(): print("Hallo") return 42 ``` But how can we basically find out, whether a function fulfils a given specification or not? **Testing.** The first approach is testing. We start the program with different inputs and check whether the outputs fit to the claimed result/effect. In simple algorithms/functions, this might be enough to clearly show the correctness. However, most problems have infinitely many different inputs (like sorting algorithms). If we really want to prove the correctness, we need to test our algorithm with infinitely many inputs - which is not realizable. Therefore, testing is a useful tool to find mistakes, but it will never prove the correctness of an algorithm. „Program testing can be used to show the presence of bugs, but never to show their absence!” - Edsger W. Dijkstra **Formal arguments.** If we want to prove the correctness of programs, we need formal arguments. The main objective is to find properties (statements) that hold during different steps of the algorithm and which then in the end imply the correctness. A correctness proof consists of finding and proving these statements. Correctness proofs might be elaborate but they are able to show the absence of mistakes. It is possible to completely formalize correctness proofs by using Hoare calculus. We will not use this approach, but many correctness proofs we see in this chapter use ideas of this calculus. ### 8.2 Loops #### 8.2.1 Invariant If we want to argue the correctness of programs using loops we have to think about the essence of a loop. Let us assume, we have a loop in our program - this could be a while- or for-loop. Then an invariant of the loop is a statement form Inv(k), satisfying two conditions¹: (i) Inv(k₀) is true before the first loop pass for some k₀ ∈ ℤ. (ii) For i > k₀: If Inv(i - 1) is true before the i-th loop pass, then Inv(i) is true after the i-th loop pass. Each loop has a trivial invariant, the statement Inv(k): true. However, this invariant will not be good enough for proving correctness of programs. In fact, finding a good invariant is not easy. At this point it is not clear, what it means to be "good". **First Example.** Let us consider the example of finding the minimum in a list. ```python #minimum(List [U]): int # Precondition: len(as) > 0 # Effect: Nothing # U is a totally ordered universe # Result: The index of the smallest element in the list is returned. def minimum(xs): n = len(xs) m = 0 for i in range(1, n): if xs[i] < xs[m]: m = i return m ``` We claim that Inv(k): „xs[m] is the minimum in xs at the indices 0...k" is indeed an invariant of the loop. For this we need to argue the two statements given above: ¹ If you are familiar with the concept of induction, then you might see some similarities. This is no coincidence. Technically spoken, every proof of correctness for loops needs some type of induction. (i) First of all, by the precondition the input list has at least one element, i.e., xs[0] exists. Moreover, since m=0 we can conclude that xs[m] is the minimum in xs at the indices 0...0. Therefore, Inv(0) is true before the first loop pass. (ii) Now, assume that Inv(i - 1) is true and we start the i-th loop pass. Hence, we can assume that the minimum in xs at the indices 0...i-1 is xs[m]. There are two cases: If the minimum in xs from the indices 0...i is at position i, then xs[i] < xs[m] is true. Then m is set to be i and finally, xs[m] contains the smallest element in xs at the position 0...i. Hence, Inv(i) is true. For the second case we assume the minimum in xs from the indices 0...i not to be at position i. Then xs[i] < xs[m] is false and the loop pass ends. In the end we have again that xs[m] contains the minimum of xs at the indices 0...i. Hence, Inv(i) is true. **Attention:** The invariant only has to be true at the beginning and at the end of the loop-block. Within the loop-block the invariant might temporarily be false. #### 8.2.2 Correctness of algorithms with loops The invariance is the main tool for the correctness argumentation. We have seen what is important to argue, that some statement form is an invariant. Having this invariant does not finish the correctness proof of an algorithm. A correctness proof involving a loop works in three steps: (I) Find a good invariant Inv(k) for the loop and argue that it is indeed an invariant. Finding this invariant is usually the hard part of a correctness proof. If the invariant is not good enough, then at least one of the other steps will fail. In this case, we have to try another invariant. (II) Argue that the loop terminates after a finite number of steps. (III) After the loop the statement Inv(m) holds for some m≥ k₀. Moreover, if we have a while-loop then the loop condition has to be false immediately after the loop. In the last step of the correctness proof, we have to argue that we get the result from Inv(m) and the negation of the loop condition. Why is this enough? First, we show that Inv(k₀) holds immediately before the first loop pass for some k₀ ∈ ℤ and by the second property of an invariant (we get Inv(i) from Inv(i-1)) we know that the invariant holds after every loop pass, especially the last loop pass. Showing that there is a last loop pass is step (II). Finally, we can conclude from the Inv(m) (and perhaps the negation of the loop condition) the given result. Its like a row of dominoes starting at k₀ and ending at m. ### 8.3 Recursion #### 8.3.1 Correctness of recursive algorithms In the functional context we usually do not have loops. Instead we use recursion to solve algorithmic problems. Therefore, we need some concept for correctness proofs of recursive algorithms². A correctness proof for recursive algorithms usually follows three steps: (1) Argue that the algorithm is correct for the recursion anchors. (II) Argue the following: If the recursive calls have the correct results/effects, then the entire algorithm has the correct result/effect. (III) Argue that the recursion anchor can always be reached. Why is it enough to show this? The last step shows the termination of the algorithm and is comparable to the argumentation that a loop terminates. If the algorithm uses recursive calls and since these recursive calls eventually reach the recursion anchor we can conclude, since the recursion anchor is correct by (I), that all the recursive calls will be correct as well by (II). Hence, the entire algorithm will be correct. ² A correctness proof for a recursive function can be understood as an induction on the argument of the function. In this chapter, we will not show the connection of correctness arguments to proofs by induction. Instead, we will just use the ideas from induction. **Second example.** We again want to prove the correctness of an algorithm that computes the minimum of a list. This time the algorithm will be recursive. ```python #minimum(List [U]): U # Precondition: len(xs) > 0 # Effect: Nothing # U is a totally ordered universe # Result: The smallest element in the list is returned. def minimum(xs): if len(xs) == 1: return xs[0] else: return min(xs[0], minimum(xs[1:])) ``` The proof works as follows: (I) If the list has only one element, we clearly can return the element at position, since this is the minimum. The recursion anchor is correct. (II) Let us assume that a recursive call computes the correct minimum. Now, if the list has more than one element, we have two cases. On the one hand, if the minimum is at position 0 and since the minimum of xs[1:] has been computed correctly, the algorithm correctly outputs xs[0]. On the other hand, if the minimum is not at position 0, then this will be computed correctly by the recursive call. The comparison with xs[0] via the min(-)-function then gives the correct element. (III) The algorithm terminates, if the list has exactly one element. If the list has more than one element, then in every recursive call, we remove exactly one element (the element at position 0) from the list. Thus, the size of the list eventually reaches 1 and the algorithm terminates.