Video 0-6: §0.3 Correctness proofs (part 2)

0:00 Introduction

0:02 this will be the second part of correctness proofs um we talked about last time already about formal verification what that means two parts proof termination proof correctness and for termination we briefly discussed this potential function method and you will dig a little deeper into this in the tutorials and what was left open was the example for lupin variants so just to recap the goal here is to show that a an algorithm that uses a loop like this this one it executes a loop it's a while loop it keeps repeating this as long as this condition is true at that point if it's ever false it jumps out of the loop and continues afterwards but if the as long as the condition is true you jump into the loop body and execute that part and then you test the condition again so uh i'm not talking about infinite while loops here uh we assume this has already been confirmed and has already been

0:33 Recap

1:21 proven in in a separate first step that the loop always terminates what i'm concerned about here is that the loop computes the correct result and usually we express what does that mean the correct result we express that in terms of a post condition so we have some statement about the state after the loop that we would like to hold true and uh you will this will become clear in in the concrete example i think um for that

1:54 to hold true sometimes you need a condition that's true before the loop that's called the precondition so it's like an assumption that you make at the beginning of the loop and um from well if that condition is true you will try to establish the post condition now if you go through this while loop this is not so easy because you don't know how often the loop will execute and you will somehow need a proof technique to prove correctness of while loops that shows you that the precondition if the precondition holds up here then a certain post condition holds down there and the the proof template for this is to find a loop invariant that's a statement that's true before while and after the loop and then you prove these three things and then together you have proven that the loop computes the correct result so let's see a concrete example of an algorithm and a loop condition precondition post condition so that this makes a little bit more sense is a bit more concrete let me move me over there for the moment i first want to discuss what this this little algorithm does this little piece of code

3:11 so it's a very simple function it computes the maximum in an array of numbers i'm sure you could all implement this and you would probably come up with something similar like this in your favorite programming language you're given an array of n elements now these comments here are somewhat specifying informally what the precondition is i just chose english text here which is fine for us remember we usually write proofs for humans the formal verification people do it they write proofs for machines we write proofs for for humans mostly and so it's it's fine if that's if it's natural language

4:00 so true assumption here is the assumption here is that we have an array of n elements and that these are numbers and that n is at least one so we don't want to call this function with an empty array that doesn't have any elements and we want to compute the largest element in this array so how would you do this well you first start by assigning the current maximum as the first one and you remember the index where you found that one

4:34 and then you iterate through all the elements by making i successively bigger and as long as i is not at the end of the array we check if the next element that we check so i is always the element that we try next if that one's bigger than the current maximum we remember this one instead and otherwise we continue indeed i doesn't remember where the maximum was found we could also remember that but we don't need that here we only return the value of the maximum all right so the post condition what we would like to have after the loop

5:11 that sounds wrong there's a what i really mean is position d here so that's after line 13. um what we want to hold true at this at this end state is what's written here in the text and using the formula from the notation from the code the variables you can express this as a as a logical statement like this the current maximum is the maximum over all the elements in the array where k ranges from 0 to n minus 1. well easy easy thing why am i overstressing this range for k here because we will use something similar in the loop invariant um but here the range is different so that's that's the important part

6:05 so the the i said last time for applying this proof template you have to somehow guess the right loop invariant and there's no easy way to do this in general um it needs experience it needs it needs trial and error necessary sometimes and i remember when i found this loop invariant i forgot the second part and then you notice the proof doesn't go through so you refine it but what i'll show you here is the end result how the proof should look like and then again you'll do a small example in the tutorials to practice that for yourself so what is the loop invariant that i eventually came up with it is the statement that the current value of this variable current max at the point where we check this condition is the maximum in the array but now only from k up to position i minus 1 and again i is the current value of this variable i that's used in the code that alone was not enough we had to also assume that i is at most n all right that's the

7:09 Proof

7:13 that's the loop invariant now we have to show a couple of things namely these three statements that appear in the template and we'll just go through these one after another and and prove those i'll try to keep as much of the code still visible while writing this down

7:40 but we'll see if i managed to get everything on the screen but we can move back and forth the first part is is the easiest one so let's start with this we have to show that the loop invariant holds at this position a in the code well what does the loop invariant at this position say

8:13 that i is still 1 its initial value that it was just assigned so what does that mean for the loop invariant the loop invariant is the same as as this statement where i set i to 1

8:29 so that's claiming that current max is well then the maximum when i is 1 this is just 0. so it says current max is a0 because that's the only element this range zero up to i minus one so by the way this is my shorthand notation for the integers

9:00 and i was eating my dots i minus 1. so that's just the set of these integers 0 1 2 up to i minus 1 but in this case really if i is 1 this is just the set with the number 0. so it claims that current max is a 0 and that i is at most n

9:36 now if if you check the first part this is just the implementation current max was set to this just before so that's obviously true and the other part and one is at most n that's the same thing as saying n is at least one and that's uh what we needed in the assumption

9:59 so at this point you see how the precondition is sometimes important we used at this point to establish that the loop invariant is true before the loop we needed to have this precondition that the array is not empty it's just this algorithm it explicitly accesses the first element so it would immediately crash with some exception or so if this wasn't the case

10:31 okay so that's both true so we have established that i holds at position a and that was actually fairly easy now let's let's see um the second part now we have to show that when the loop invariant ends the loop condition which is which is this here i is strictly less than n those two together if they hold at b then at c we again have the loop invariant that's the the

11:06 important part of the proof and it's slightly more complicated than the first one so we apply one of our proof templates from before we do a case distinction and there's there's two cases the first case is that the next element that we look at is actually bigger than current max and you see this uh case distinction exactly follows what can happen in the code there's this if statement and we somehow have to deal with the two possibilities how that if statement comes out so if a i is bigger than the current maximum which we know from the loop invariant is is this

11:56 4k in 0 up to i minus 1. it's this maximum of the array and here we use our loop invariant because that's saying exactly this with the current value of i

12:24 now in this case we enter this uh this this statement the thin then branch of the if statement and that means our current max is equal to a i

12:52 after this line nine now i have to be careful not to say line 10 because uh here we change the value of i so that changes this statement because it involves i but then again

13:12 after we increment this after line 10 we have changed the value of i but still our loop invariant is true because we have made that range one bigger but we also included one more element

13:48 so that still holds now i is one bigger but we know the the maximum in this range up to the old value of i that one was actually our a i minus one it's the last value that we just inserted there all right we also have to establish the second part of the loop and variance so we always have this these two parts though there's uh first part and the second part so that means the first part is is fine um for the second part remember we also have the condition at b and that was saying i is strictly less than n which is the same as saying i is at most n minus 1 because we're dealing with integers here and the only thing we do in in the loop body is we increment i by one so in the old state that would mean i plus one is at most n

15:06 and because we make i just one bigger here at this position c we still have i at most n and that's our green claim so we re-established the loop invariant after the while loop

15:27 Summary

15:31 so that was um that's usually the the toughest part to show that the loop invariant is re-established after the body of the while loop um once we have done that we have shown that the looping variant is indeed a useful in is is a valid invariant so it survives the execution of the loop if it was true before it remains true throughout and is still true at the end now the last step is to show that the loop invariant is actually useful in that the statement that it still holds after the loop guarantees us something interesting and that's the the last point that we're going to show so the the third point here formally is

16:22 wrong color that the first the third point is that the loop invariant the third point is that the loop invariant plus the negated loop condition which means once we leave the loop so not condition is nothing else than saying i is at least n

16:51 so the third part is the loop invariant and this i at least and thus that implies our post condition which remember was current max is the maximum of the entire array the array goes from zero to n minus one that's that's the entire array now again not loop condition that's nothing else is saying i is at least n but the blue part from i said i is at most n those two together clearly mean that i is equal to n

17:28 and that means the red part in the loop invariant says current max is the maximum for k in 0 up to i minus 1 but i is n so that's n minus 1. ak

18:00 and that finishes the proof which mathematicians like to show by drawing this little box um so again we followed these three steps we showed that the looping variant is true before the loop it remains true throughout the loop and at the end we show if the loop invariant is still true it implies something useful in this case that current max at the end is indeed the maximum of the entire array and that means the function that we that we have here computes correctly computes the maximum that concludes this first unit 0 on proof techniques you will practice a little bit more in the tutorials but i hope you will find these proof templates useful for the future in this class and outside of it