Video 0-4: §0.3 Correctness proofs

0:00 <Untitled Chapter 1>

0:03 in the last section i want to talk about correctness proof so bringing the all the talk about proofs and proof templates back to algorithms and computer science and i want to go through one example in more detail so i might might sit down for that part uh the the idea here is give you a glimpse of formal verification

0:17 Formal verification

0:27 and verification is a fancy word of in this context saying prove that a program is correct and correct usually means two things it terminates and it computes the correct answer both of which usually prove in isolation but

0:49 we we take them together as the statement the program is correct although former verification is not our focus in this module some of the techniques are useful for us because we do want to derive efficient algorithms and sometimes something is obviously fast but not completely clear why it does something useful or even correctly computes what we specifically want and we will sometimes borrow some of the ideas from this to convince you even though maybe a very formal argument we will usually just sketch

1:33 so we have two things that together mean correct um and as i said we proved them separately so guess what there's a different proof template for each of them

1:48 Proving termination

1:53 the first part is about proving that some program you wrote eventually stops now you may know the halting problem and the undecidability of that and so we can't always given we can't write a program to do that for us that given a program tells us whether program halts but that doesn't mean that you can't do it with a specific program because you're not a turing machine and for the examples that i have in mind it's not like someone gives you an arbitrarily complicated problem program but you design one so for those ones we hopefully are able to prove that they terminate and here's here's a proof template how you could do this and i formulated here as as a potential function um which sounds really fancy in all the greek letters i think the concept though is is actually quite intuitive uh what we'll use at the end of the day is that if you start with a natural number and you make it decrease by at least one because it's an integer in each step if you make it strictly smaller in each step after a finite amount of time you will reach zero so if you can somehow prove that the parameters of your program if it's uh it's formulated for a recursive program

3:08 here so you have some some procedure proc that has parameters and it calls itself recursively maybe many times but if you can show that somehow these parameters get smaller in a certain sense and you stop if you reach zero then you're you're done then you have proven that it always terminates i might stress that this is not about proving something how fast it terminates it's just about whether or not at all it ever stops

3:45 okay so we define this potential function that can be just any function you can come up with it takes the parameters of the program and it computes some natural number and here it's important that it's a natural number not just an integer so i'll write n0 for natural numbers starting at 0.

4:13 so this potential is always non-negative or weakly positive and the the thing that the proof template tells you to do is prove whenever you have a recursive call so you would have to think about it that there's some code i don't know python code um where there's something done and then there's another call to the same procedure again

4:44 with some other parameters that you compute from x probably and then you keep going and there's also some some place where you return so you look at your python code and you see if there is a recursive call and if that's the case you try to show that in any such recursive call as it's as it's shown here the potential of the parameters of the recursive call are strictly smaller than the parameters of the call you started with

5:17 what i didn't put on the slides but what's hidden here is essentially a big for all x1 x2 up to xm it's an all quantified statement again you want to show for all choices of the input parameters every recursive call decreases the potential okay

5:37 and that's yeah that's as far as the template goes uh then the the second part is is easy if you've shown this then if you whenever you call the function there's some potential that you start with and it only ever gets smaller and it has to go down by at least one in each step so it will reach zero after a finite amount of time and actually you could say the potential even bounce the running time but we we don't focus on that in this unit

6:07 okay um [Music] i formulated it here for a recursive function instead of a while loop but as you may know uh you can usually write one in terms of the other or vice versa you can translate from one to the other and you can adapt the template for loops in in pretty much the same way you have some point at the beginning of the loop where you say now i measure my potential in terms of some variables and then whenever the loop runs one more time that potential has to decrease so same conceptual idea just slightly different formulated you will do a detailed example in the tutorials so this is all i want to say about termination proofs for this unit

6:56 Loop invariants

6:59 so what's left for us is the second part which is i think a little more subtle that's why i want to go through that in detail that's the the correctness part that you compute if you ever terminate you compute the correct answer

7:17 and the template for this uh so-called loop invariants um okay i should have put this on slider anyone uh seen calculus one two a few more poor calculus for proving statements like this and loop invariants et cetera so tony hoare invented this this way of uh proof templates for for correctness so it's named after him the same same person who invented quicksort if you're interested in these historical facts okay the template works as follows you have a code fragment like this on the left here there's a while loop um and again now we're we're not concerned about termination we already assume that this terminates the question is what does it compute for us and there's four interesting points it's directly before the loop just at the beginning inside the loop body but at the bot at the top the same thing at the end of the loop body and then again after the loop straight after you terminate from the loop there's another interesting point in time or in code and so the template tells you you should find a loop invariant so i is some some statement about the current value of variables can be some complicated construction again

8:44 the template doesn't tell you how to find the loop invariant this is up to your creativity imagination ingenuity this is usually what's what's challenging but the template then tells you if you have found the correct loop invariant you can prove the following for uh three things and then um you have proven a certain a certain statement the first thing you want to prove is that the invariant holds at a before the loop starts then you want to prove the invariant plus the condition that tells you whether to continue the loop those two things together imply that at the end of the loop body the invariant still holds or holds again

9:33 and the third thing you should prove is if you take the loop invariant and you add the negation of the while condition so which is another way of saying the loop invariant together with the fact that you stopped the while loop that together implies the desired post condition okay we'll we'll have to see what this means but the the statement we're trying to prove here is if before the loop something is true so we make some conditions if you want to reach this piece of code you should make sure please dear user make sure that certain conditions are met and then i promise you if you keep your promise i promise you that after the loop something else holds and we're trying to prove this implication if the precondition is fulfilled before the loop then this condition is true after the loop uh what these two conditions are is again up to you it depends what you want to show but this will be clear in the example i think

10:38 so that's that's the template magically find a loop invariant i don't tell you how just do it and then check that these three things are proven okay that's what the template says

10:50 Loop invariant - Example

10:53 and so let's look at this example together where we apply this on a concrete example it's a simple procedure you can maybe read over it you've probably written something like this in in some programming language so it's given an array a and the length of this array and you're trying to find the biggest element in that array it's really fancy and complicated and the function does the obvious thing it it loops through the array keeps the current maximum and at the end spits that out it's probably what you would have done if i would have told you to program this i know that many languages have something built in to do this even but let's pretend you don't have that so the point is not that this is an interesting algorithm the point is that we want to prove such a correctness for this for this piece of code and so here you see it's it's usually easy to come up with these pre and post conditions if you know what you want from this function sometimes the edge cases are a bit tricky so the precondition means you can only call this function for certain values and here what we want is that the array is not empty we insist that there's at least one element in it

12:10 and indeed if you think about it computing the maximum of an empty array is a bit pointless and it's not clear what you should return so this is kind of reasonable but we don't make any other assumption uh other than that array elements can be compared um so there's there's a point here where we use a comparison operator to compare two elements from the array and we assume that this is somehow well defined so maybe it's numbers

12:42 maybe i should have just set here integers or so to make make life a bit more concrete but it would work for anything where you can compare and so the only real restriction is i want an array and at least one element in it that's a weak precondition doesn't require much uh the post condition is a bit more interesting it says the output of the function whatever you return is the biggest element in the array so here i just said the maximum element in the array if there's several maxima we don't really care we could strengthen the statement because that procedure will probably return the first of these occurrences but maybe it's numbers and they're all the same so it doesn't matter okay so

13:33 i don't know if it makes sense to write this down i don't think i have the precondition on the slides so let's let's say and then uh the post condition for the entire function is that the output is the maximum element so that's that's what's written here

14:33 so let's let's see how we apply the templates um let's first pick the easy parts the loop condition what i call con before that's just this part what is here in the loop so we just copy that out

14:53 we can work our way back up so here we return current max so if we translate just the post condition i i showed here you can hardly see this move right um

15:12 that's much better i could use the mouse well next time i bring a mouse um there's a tiny little dot that moves can you just barely see this if we take this post condition and we replace output with current max then we get what's written here so that's what we want to hold in line 30. okay

15:41 uh and i also already solved the tough part of finding a loop invariant that's this one here now if you look at this loop it iterates through the array so you have seen a prefix of the array and current max is the current maximum of this prefix so this this first part is maybe quite intuitive if with the current value of i you want that current max is the maximum in this range up to i it turns out it's excluding i itself what's maybe a little more mysterious is why you have the second part you also require in the loop condition that i is never bigger than n that seems a little less clear where this comes from and the answer is you try with the first guess that sounds intuitive and you see it doesn't go through and then you keep adding things to the lube invariant that's how you get to this and that's how what i what i already did

16:43 um so with this set the template tells us to prove these three things um so let's let's see how we do that for the first part we have to prove that the invariant holds at position a

16:59 so we look at the blue at the looping variant at this point we have just set i to 1 and we have just set current max to the first element in the array so yeah one thing i should have mentioned uh arrays always start with zero for this module wherever it makes a difference i think that's the convention in java and in python and in most languages that makes sense r is different in case you know about that one but most most languages start with zero so that's the convention i also picked

17:50 so this is what we've just done in the line before so if we just plug that in into the statement of the loop invariant we see that current max should be the maximum over all k between well what is this k between zero and zero okay i can do that

18:22 because that's a single element it is just c a zero a of zero and so that's that's correct because we just set current max to this value okay so that's the first part let's maybe

18:41 and we have a second part that we can mark in in blue so that means the red part is is proven clear how about the second part well for that

19:18 so i is also at most n and that proves the the blue part okay so that's the kind of baby steps uh if you want to go uh all the way to the details how you can prove this now let's look at the second condition this is the more interesting one what happens in the loop body um so we'll need a bit more space for that but

19:47 i'll probably have to scroll back and forth to the code we assume that the loop invariant holds at the beginning of the loop body plus also the the condition the loop condition which again was i is strictly less than n if you remember from here

20:16 and now we want to show that the loop invariant is re-established at point c now the trouble is that various things change in the duke body in particular we might reassign current max and we definitely increment i so you sometimes somehow have to deal with that

20:35 and here's a good case where we can distinguish what happens by looking at what the if does and the first case is that the maximum in the prefix we're looking at at the moment so from 0 up to i

21:11 is at this last position okay in that case we enter the if statement because then so um so that's the that's the first case and we'll have a second case that we have to deal with later

21:34 and that's that the maximum is not this value that's case two for case one we intuitively intuitively know we will enter this if statement but how can we prove this from what we know formally namely the loop invariant and the condition

22:04 the loop invariant implies that current max is the maximum up to i minus one okay so it's important to stress that here we want up to i and here it's only up to i minus one

22:39 and we know in this case that the maximum of this of this range is the last element i think it's more convenient to write the case distinction like this this new element is bigger well it's not

23:45 so we still have a valid case distinction but i changed the case distinction that's what often happens if you do proofs so i can get rid of that red part though so we know current max from the duping variant um is the maximum in this range so this condition this this case immediately tells us that then current max oops now what i wanted current max is strictly less than y a of i

24:24 that's just using this equality in and the the case and the the condition of the case and that's the condition asked in the if statement okay so we enter line 9 and change current max

24:56 so after this line current max has a new value and it's a a of i and then after that we always increment i no matter what and so now we're at the point where we want to go now we have to show that the lube invariant holds again so we want to derive from this that i holds again

26:11 and um if we take the the case assumption that means i don't know uh i take this statement that implies that if i take the one bigger prefix this is a of i because the next value a of i is bigger than all the previous ones okay

26:55 now the annoying part is that i keeps changing the values so we have we have to pay attention uh where where which which i we mean the one before we change to the one after we changed it we might want to give this a prime just to make sure that we're talking about the new one the new value of this

27:21 variable so if you look at this if you just insert what i prime is here then this is exactly the same term so these two are the same and we've just set current max to ai so these are also the same

27:40 so in this case we've re-established the first part of the loop invariant the red part and for the second part we need the loop condition which again remember that loop condition was i is strictly less than n

28:08 i was strictly less than n so i prime is still at most n because we just added one and so that's that's this uh second part that we wanted to prove okay so in case one we've reestablished the loop invariant at the bottom of the loop body we still have this um the second case to deal with should have left a bit more space but

28:48 the second case is actually easier because the one where we don't need the if statement if you look at this condition it means that this new element is not a new maximum

29:27 well that's true but that's not helpful uh we want to use the lubin variant so by i we know that this is the current value of current max which means in the code we don't enter this if statement

30:25 so our new value for current max is the same as the old value we don't change it that's the first part but we do increment i so we have this

30:42 i prime is set to i plus one uh and now we just look at the loop invariant again and see what has changed uh we take this part then that just includes the value i but that one is smaller than the previous maximum

31:41 and that was current maximum and so it's still current max prime okay we need more space because current max prime is the same as current max and current max by the loop invariant was this maximum up to i minus one

32:00 and if you check this is the red part of the loop invariant over here uh and for the second part the same argument is true the the blue part nothing has changed uh n is still um we still have the loop condition that i is strictly less than n and we increment it by one

32:32 okay so that concludes the proof of the second part we've done this one we've done this one what remains is that to show that at the end it has actually helped us but that's that's much easier

32:55 so we take our our loop invariant and we add together the negation of this condition so a last time current max is a maximum for k between zero and i minus one

33:23 and we have i at most n and the negated loop condition so not i is strictly less than n means i greater equal n okay and now these two things together if i is at most n and at least n it can only be n

33:50 and that means we can insert the value n for i in the first part so if you insert this one here then you get that current maximum is the maximum of the array from zero up to n minus one that's the entire array okay

34:35 so that was the somewhat longish proof uh that if you start with an array and end at least one you end with actually the maximum this was a tiny example uh and it took some back and forth with the cases and almost half an hour to spell out maybe if i prepare it without making mistakes maybe i can squeeze it into 20 minutes with the same explanation but it's still quite tedious right so we will usually not go all the way down to these steps but any proof you write should be possible to be expanded like this otherwise it's not a real proof you will have some gaps in there questions

35:17 [Music] yeah the question was um i'm assuming that the array is ordered uh yeah in a sense the code doesn't make sense in at this point uh we compare two elements from the array and if that comparison doesn't have a meaning then uh the code doesn't have a meaning so that's why i smuggled in the precondition that we have a set of num an array of numbers where the comparison is clear but it's a little more general whenever you cannot define a comparison it's fine but we need that assumption yeah

35:57 all right good uh that's all for today that's all for the proof techniques uh on monday we'll start slowly with getting to models and machines um more on the algorithmic side and we'll start next week with data structures as well have a nice weekend see you on monday