Video 1-4: Correctness Proofs

0:01 In the next section we'll look at correctness proofs, the first of two things that we may want to prove about an algorithm, that it computes the correct result. This is a whole a whole area called formal verification that maybe lives through a slight renaissance these days because it used to be extremely painful to write these specifications. AI can help a bit with that. Uh the main main challenge still remains that the formal proof you only get for what is written down in the specification and it's still up to you to check if that is what you wanted to claim. Uh but that's a the general area says, "Here's a piece of computer pro computer software program and I claim that it does XYZ. Let's prove mathematically rigorously that it does." So I only want to give you the flavor of how this is at all possible or how does such a kind of proof can look like.

0:57 Um and we'll not dig too deep into it. Uh there's technically two parts that you want to prove separately for most programs. One is that the program on a valid input always terminates, so it doesn't run into an infinite loop. And then the second is assuming that it does terminate, if you've proven the first thing already say, then um it also computes the correct result. Uh we'll look here at a specific example of of a a while loop and show I'll show you the the template for how to prove formally that a while loop does what it's supposed to do. You can translate the same to us most of the other constructions in a program. In particular, recursive uh functions are loops in disguise if you wish. And all the other parts of a program that are not loops are rather easy to deal with. So loops are the only really uh um parts that needs um a clever insight to prove them correctly.

1:59 But let's first look at the termination. Uh, suppose for for this that we have a recursive function. That is a bit easier to state. So, I have a recursive procedure that I can call, say a method in Java. Um, and it might call itself. So, the question arises, maybe this keeps on calling itself and never terminates, or in Java uh, dies with a stack overflow.

2:28 Um, now if it calls itself, it will hopefully have some parameters that get changed. Otherwise, it's certainly an infinite loop. So, the general setup could be some procedure proc has uh, m different parameters that you can pass values to. And we want to prove that this terminates. For that, we define a potential function, which is just some abstract mapping that takes values for these parameters that we call the function with and maps them to the uh, natural numbers. And you see again, natural numbers keep popping up because they're well-founded set. Because uh, we'll require that this potential um, is decreasing in any recursive call, gets strictly smaller. >> [snorts] >> So, um, formally, whenever I have some uh, now let let me sketch this procedure this definition, then it does some things. And then maybe it calls itself on some other parameters here, this y1 up to ym. And then maybe it does some more things.

3:39 It could also call itself another time with some different parameters. The important thing that we want to show is that at any point where the function does a recursive call, these parameters that I use in the call are such that the potential at these values is strictly smaller than the potential of the original call where they came from. So, I'm starting here with some potential and here the potential in the recursive call has to be strictly smaller. And what that means, because the natural numbers are well-founded set, I can only strictly decrease any natural number I start with a finite number of times and then I'm at zero. And then, if this is true, the function has to terminate. There must be some some other if branch that does not do the recursive call. So, at at this high level of abstraction, I think this is rather obvious that this is um a way to prove that this terminates. The trick is in finding this potential function to do uh to map to the values of the map to the functionality of the of the recursive procedure that you're looking at.

5:02 Um I explained this here for a recursive procedure where it's a bit more obvious that you have this this recursive call, but the same concept applies to a loop. We can you can also define a potential function that somehow takes the uh variables in the environment or in the uh in the state of of your program and maps those to a some number, some integer. Natural number. Uh and when when if you can show that after every iteration of the loop, this potential drops by at least one, then again, it can't keep going forever because the natural numbers are well-founded. Uh you'll see a worked-out example in the tutorials where you'll you'll uh prove an example uh code to terminate in the tutorials using this and then maybe it will be a bit more concrete.

5:56 That's termination. That's fine. It's kind of necessary that programs terminate to produce any sensible output. I want to spend a little bit more time on the correctness part. Because termination after all is still a binary question. Either it's it stops at some point or it doesn't. That's still easier. How about proving the correct output? And for this um we'll basically focus on on a single loop. Um the general setup if you want to read into this, I also linked some a very lengthy document on the website is called Hoare calculus or Hoare calcul.

6:45 And this has essentially the following um setup that you always have some precondition. So a statement about some uh about the state of the variables of a program, then there comes the code of the program. And then there is a postcondition.

7:14 And these these um triples in in Hoare calculus precondition um an instruction and postcondition always mean that if the precondition holds before the execution Uh by the way, this is named after Tony Hoare, the inventor of quicksort as well, who passed away earlier this year. Um one of his main main contributions or areas of of uh research was in formal verification. And he came up with this clever idea that essentially this is all you ever need to do to prove a program produces the correct output. It's enough to do in general these kind of uh statements. If something is true before the execution, then I execute some program that might change the state of the variables and so on, then something else is true afterwards. By recognizing that this includes all statements, P can be any any instruction, and it could be a return instruction. So, you can uh use the same template to prove that a function returns the right value, and you can even uh P could be a function call to some other function.

8:48 So, you can make this um P arbitrarily complex, and it's still has the same kind of uh uh schema. And then Hoare calculus is about how do you get from a triple of this type with a small instruction to uh piecewise larger programs. And all of the steps uh you can imagine if you have some precondition, and then you execute some assignment that sets a variable to a new value, then in the postcondition certainly the variable has to have this new value. And so, as all of the other instructions are rather straightforward, you can work backwards from the postcondition to the the weakest precondition that ensures it, except for loops or recursive calls. There it seems you need an additional creative ingredient.

9:39 And that's called the loop invariants. Uh for for a loop, the general template is there's some precondition before the loop and we would like to have some postcondition after the loop. Uh but we don't know how often the loop is executing in general. So we also need two other positions uh just above the body of the loop and just below before you go into the repetition.

10:06 And then you often need to find some specific uh statement about the variable. I'll make this concrete on an example in the next slide. Uh you have to find some uh condition that is true before and while and after the loop. More precisely, it's true before the loop starts. It's true at this point B. And if it's true here together with a loop condition, then it's also again true at point C. And then you can follow from that that it is true after the loop as well. And from that you can work out again uh these pre- and postconditions where now P is the entire loop. Let's um let's see an example of that. And let me take this with us.

11:02 Uh here's a little example program. It's not a very complicated piece of code. Let me step through it though so that we're all on the same page. Uh it's called array max and hopefully does precisely that. We compute the maximum entry in an array. And here's already an assumption stated that the number of entries in the array is one, so it it has a well-defined maximum. It's not just empty. Uh how do we do this? Well, hopefully the easiest and uh simplest idea that you would also have come up with. We initially say the maximum might be the first element at index zero. Um I have a variable that I'm going to loop over. While my index, as far as I have have come in my array, is not at the end, I check if the next value is larger than my current maximum. If so, I update my current guess for the maximum. Otherwise, I do nothing and I always move on to the next element.

12:04 Once this loop has terminated, current max is the maximum over the entire array. That's the intuition anyways. The code This is code that you've probably written 500 times of one for in one form or another. In Python, you don't even have to. There's a max function built-in that does this. Uh but I think the the code is is obvious enough that you would believe me if I told you this computes the maximum. Let's pretend to be super pedantic and not believe a word. Also, are there maybe corner side conditions? Uh stuff like this. Um what happens if n is zero? Uh you can reason about it in this case. There's only so many things in this tiny piece of code that can go wrong. But I'll show you that you can rather make mechanically arrive at all these corner cases and conclusions. Okay.

13:05 Let's keep this here on the side. Um we'll have to map our our specific code to the template here. Where of course there's only one loop, so it's rather clear which maps where. Um uh just as a reminder that this is the same thing as we had uh on the previous slide. Uh the condition of the loop I've already plugged in. This is just this test whether J is strictly less than N. And in all these Hoare calculus proofs, you always work bottom-up. You work backwards through the program. Because I kind of want a certain thing at the end. I know what I what I intended the program to do, namely compute the maximum. And because I'm returning the max this this variable current max here, what I really want is this post condition. I want the current maximum at the end is the maximum over the entries in the array where this index K is between 0 and N minus 1 inclusive.

14:11 Now to prove that, um, we need to guess a loop invariant, a statement that helps us get this, uh, template proven. And unfortunately, there's no mechanic way to find the loop invariant. You can make educated guesses or maybe, uh, you can have someone suggest one and then check if it works. It's usually an iterative process.

14:31 Uh, here I've already worked it out for you, so we don't have to do it in iteration. Uh, but it really has two parts and the second one I first forgot and then you notice during the proof doesn't go through. Uh, and then you know how to, uh, um, to fix it. Or you you hopefully see how to fix it. So it has these two parts. The, uh, invariant should be true at all points in time that or, uh, at these designated points in the program, that the current maximum is the maximum of some prefix of the array up to this, uh, index J, which is our variable. So this keeps changing all the time, right? The the claim of the value of J changes, so the claim that this invariant, uh, makes also to keeps changing. Uh, and the second part is just that J is at most N. Now, is the invariant true at A?

15:30 Well, let's look at it. Uh What are we claiming here? If we insert what J is initially, J is 1. So, we only consider K in this range from 0 up to 1 - 1.

15:56 And so, what this uh magenta part of the invariant claims is simply that uh current max is A of 0. And that's true because precisely we've set it like this in line four.

16:23 And also, the second part um J is at most N. That's a bit tricky. We don't know for sure uh if there weren't any other things known. But, we set J to 1, and we know N is at least 1. So, it is true here.

16:45 So, we've proven that the invariant holds at this point A at the beginning of the loop using either things that were done in the program just above there or were assumed as the precondition of the entire method. These things that I'm I'm writing here, these are these are kind of assumptions that the procedure makes to who whomever this procedure is called from.

17:09 Okay. Now, for the other two parts, I'll need a bit more space. For the sleep deprived where the short-term memory doesn't work properly, let's copy everything.

17:50 Now, let's look at this part two. We're trying to show that uh if the precondition holds at the beginning of the loop, together with the loop condition, this implies that at the end of the loop body, we have the pre- the uh loop invariant reestablished.

18:11 Let's rewrite what this uh invariant was. So, the current max is the maximum over this. Let me write this a bit more concisely with round parentheses for the excluded uh right-hand side.

18:29 And J less than or equal what n. That's the loop invariant. Now, we also have this loop condition here. And that was just J less than n. This is literally here from the code. So, from that, we're supposed to deduce that at the end of the loop body, we have this loop invariant reestablished. Now, the code here does um a few things. Try to make this a little bigger.

19:03 Of course, now these are no longer where they're supposed to be. What the loop body does depends a bit on what value we have. So, uh let's do a case distinction at this point. Remember we're trying to prove an implication, this one? One of the templates was we do a exhaustive case distinction. So, we add another condition and its negation um to the precondition and try to in both cases follow the um conclusion. So, the case one that we'll look at is that this next element in the array is less or equal the current maximum.

19:44 Then the second case will be the converse that it's strictly bigger. In this case, if A of J is not larger than the current maximum, I do not execute this update. So, current maximum stays the same value. Right?

20:02 So, my AJ less or equal the current maximum, this is by the loop invariant which we assume here, and maybe could make this in pink. This is this maximum over the range up to J excluding J.

20:28 But of course, if my AJ is not larger than than the maximum here, I can include this as um another option for K without affecting the value of the maximum.

20:44 Let's maybe make this highlight this a bit. That follows from the case distinction. And here you see why the case distinction gives you more power. It allows you to tease out what happens in both cases. Now, after this um if condition, we also increment J.

21:04 So, I should say this is at line nine, after line nine, where we've updated or we didn't do anything to current max, but we haven't updated J yet. After line 10, the same condition is still true, but now J is one bigger. So, I get my my formulation from the loop invariant back.

21:38 And it looks superficially like it's the same as before, but of course J has grown, so it includes one more value. And you can see that this These are the same subject to J changing value.

21:55 Now, that proves the the pink part of the loop invariant for this case. Um let's also look at the green part. Uh because this orange part is strictly stronger than this green part, this is where we uh start at B.

22:21 That's from the loop condition, otherwise we would have stopped. So, that means J, when it's strictly less than N, it can be at most N minus one. Now, after we've incremented this J, so this is again uh after line nine, if you wish. Now, after the increment, we're back to only J less or equal N, and the minus one is eaten up by the increment. But, this green part is what we needed for the invariant, so we've proven that part as well. Okay?

23:01 That was case one. Uh we also need case two. Let me try I'm I'm not going to smuggle it here. Let's put it below.

23:26 This means the loop invariant is restored at this position C in the code. Now, for case two, we have the opposite of case one. Aj is now strictly larger.

23:43 That, of course, means that Aj is the maximum of Now, if I'm in this case, then I go into the if branch and I update current max to this value.

24:19 And so, again, I have the statement current max is this the maximum including this J plus one. That's the very same thing we had written up here. So, by the very same reasoning as above, I get the same conclusion. All I that I've marked here is literally the same as in case one.

24:42 So, let's here be a bit lazy and say Using the same argument, I get that my loop invariant is reestablished Okay. That proves this second step that the loop invariant is restored throughout the loop. We still have to prove the last part, but this is uh fortunately much easier. Namely that um what we get at the end of the loop already is enough or is is indeed what we wanted. So um that we can smuggle up here because it's also the thing you want to check first to make sure that the loop invariant is strong enough for what you try to claim. At the end uh we have this loop invariant, this part, but we also have the negation of this condition.

25:45 Not J strictly less than N. In other way In other words, J at least N. Right? And so these two together of course mean that J is equal to N.

26:05 At this uh point D in the code. >> [snorts] >> And also we have the loop invariant. I is also true. So this magenta part Here I'm going to be lazy again.

26:28 So this where you insert what we've just learned about J. Love the combination of colors. This implies what we wanted to prove. Namely the post condition up here is now precisely this up to my uh syntax difference. And so this is what we wanted to prove because it's the same as this.

26:55 Okay. So, to reiterate, uh relatively simple piece of code, and it took us, I don't know, half an hour to go through the full details. We will not do this many times in this lecture because we won't get far in the interesting algorithms. The point about this about this whole section on proof techniques is that in principle, it is always possible or you should always be able to go to that level of detail if ever needed. And maybe some parts of this can be automated. What cannot be automated is finding these loop invariants because there's nothing in the code that tells you precisely what should go there. And this is more than more an art than uh science or or uh engineering to find these loop invariants. But once you have it, the rest is a relatively mechanical proof.

28:01 In the next section, we'll look at the second kind of proofs we'll do to algorithms, namely about estimating their running time. We'll look at that in in much more detail. Uh I wanted to briefly wrap up with um something that I started this lecture with, namely this this shuffling algorithm. And I've um I've mentioned this informally, and I thought it's worth showing again why this um why this shuffle can't uh can't work properly.

28:43 And that's what's behind this proof, but let me first show you what happens. So, we've we've observed that with this with this broken um shuffle method here, the reason ultimately why it's wrong is that the uh set of possible random events doesn't match the number of permutations. To make this a bit more obvious, what we can do, and also what's behind the computation on my slides for the exact probabilities, is you can you can turn this around. There's only a finite me- number of possible dice rolls. And each of those you can simulate the program for and see which permutation it produces. For example, you can take this this first one, all the uh dice show zero, or all the indices that are swapped with are zero, then you end up with this array 4 1 2 3 at the end of the four iterations. What What this shows here is after the first iteration, that's the array. After the second iteration, that's the array.

29:45 Third, fourth, then I'm done. I'm doing this here for four elements. That's the first option for these random outcomes. And I can take any of the others, and they all fall into one of the permutations. Right? Each of them modifies a bit what the outcome of the permutation is, and I can keep tallies how many go where. And let's speed this up a bit uh the other direction.

30:13 And you see, once this fills up, it just doesn't end up being [clears throat] uniform. Each of these configurations has a probability of 1 over 4 to the power 4, so 1 over 256, I guess. Um and that doesn't nicely divide with the 4! 24 permutations. And you find that some are more more likely than others. All right, same picture. Whereas if you go to the Knuth-Fisher-Yates shuffle, the one where here this goes from I to N. You can do the same. And this time uh each of the permutation occurs exactly once. Which is a hint for how to formally prove this. This is just uh showing by example. This gives you an intuition. It doesn't formally prove anything. But the fact that each random outcome corresponds to precisely one permutation of course implies that it's uniform. If you can formally prove that indeed there's a one-to-one correspondence, a bijection, between these dice roll patterns and the permutations at the end, then you're done.

31:24 And that is indeed what you can do. Um Uh it's spelled out here on the slide and I'm going to go through it in more detail, but I thought it's it's maybe good to wrap up this in in in initial example with a formal proof because uh I kind of left it there without doing that. Okay.