Video 0-4: §0.4 Correctness proofs

0:02 after we talked about mostly mathematical topics that are not so directly connected to our our main area of algorithms I want to bring it back to the more computer sciency part of proofs and again the purpose there is is is is on one side showing you some really formal techniques that make such statements uh or the proofs U very rigorous um although we will not use them in all the full gory details uh that's the kind of thinking that you should develop when you think about algorithms and argue why they are correct um so that's that's part of this last section in this section we'll discuss proof techniques or templates for showing the correctness of programs and what that even means in in our case this is the a whole area called formal verification which is really not the focus in this modu modle um but a little glimpse of it is part of every algorithm design when you design an algorithm for an algorithmic problem you want to make sure that the algorithm is fast but it's only useful to if it's fast if it's also doing the right thing and so uh implicitly we always want to a correctness proof as well at least informally um in formal verification the the correctness of a program is split

1:28 into two parts one is that the program terminates so at least eventually it halts it stops running which is uh a far cry from being efficient and we'll spend the rest of this module on efficient algorithms but for this for this section it doesn't matter how long it takes as long as eventually it it stops running that's at least part of the game and then when it when it stops running our assumption is all algorith are essentially boxes that take some

2:11 output I'm sure you have seen this box many times but the implicit assumption among this I mean there's there's some computation going on inside of here these are Wheels obviously uh not sunny side up there's some computation happening inside there and it's supposed to produce an output well it can usually only use an output when it stops running or it would have you would have to Define what that otherwise means so the second part is is about producing the correct output when it

2:46 stops now we'll um we'll restrict it to a specific part of the program uh here but it it is actually more General than that so uh you can you can use it on different parts of the program to generalize it the the general template if you want to prove a program terminates is uh something like um like a potential function argument uh that you may have seen uh in this case I'm I'm assuming we have some recursive procedure so a function that calls itself maybe if you take a step back why would a program ever not terminate well it it only doesn't terminate if it somehow gets into an infinite Loop of some sort and that can either be a while loop while something is not true keep going and if that never is true then it it is stuck in that Loop forever but it can also happen in a recursive function that keeps calling itself and never stops in a way these two are equivalent if you've had some some more uh theoretical computer science modules you'll maybe even have proven that you can translate one to the other um and back uh but these are these are the two main reasons why a program might never finish infinite recursion or uh an

4:04 infinite Loop and so for for the proof here we'll assume that there's a recursive function some procedure proc that has a bunch of parameters uh and it might call itself at several places in the body so what we'll do is uh we'll Define to show that this eventually terminates we'll Define some function that takes the parameters of this of this procedure and converts them somehow into a number and how exactly that works doesn't really matter so much uh you'll have to pick a concrete example and you will do in the tutorials next week um on on how to make sense of what the how the parameters turn into a number uh abarely speaking the potential is some function that gives you a natural number back for every set of possible parameters for this for this function for the procedure and uh because it's a natural so I'll use this n Zer as the set of natural numbers 0 1 two and so on and I'll try to use n without the zero for the same thing but starting at

5:22 one if that's important I might I might actually write with a subscript greater equal one to make it more more clear so this potential is at least Zero by definition there's no smaller natural number what we have to prove to prove termination is whenever the function calls itself the potential of these parameters that it calls itself with is smaller strictly smaller than the potential of the parameters it was called itself so uh in other words at least the potential drops at least by one again because it's natural numbers if it's strictly smaller it has to be at least one smaller that's pretty much all for the abstract template again you'll flesh out in an example how this works next week uh but that means the procedure has to terminate because it has to start with some some finite value namely the potential of the initial parameters that it's called with and whenever it calls itself something strictly goes down you can only do that a number of times in the integers then you you flat out at zero and you can't can't go further h a similar idea works for Loops if you have if you have a while loop then there will be some parameters there some variables so it's not as explicit as in a function call but you will still

6:47 have variables that change their value over time and so if if the fun if the while loop eventually terminates there must be some way to get a potential from the variables that always decreases so it's it's kind of um it works in both ways but the the trick is to find the potential function depending on how complicated the code is that's quite a formidable task again I'll refer you to the tutorials for an example what I'll show you in detail in the rest of today's session is uh for the second part how do how do we prove the correctness of a piece of code so let's let's assume we already established it does terminate what does that even mean for the code to be

7:41 correct the way this is this is almost always formalized in the form of for logic is that you run a program um maybe it's worth worth writing that down you run a program program assuming some conditions that are true so for example that your input is of a certain form you don't accept arbitrary bit strings you want certain structure for example you may have a function that takes a number and the number should be at least one I'm making this one up but that could be a precondition then you run your

8:24 code so this could be conditions on the variables on the then you run a piece of code and you try to have a formal implication that the preconditions with the code imply a post

8:52 condition which again is some some statement about the variables and the for most for most types of programs this is relatively easy to do if you uh if you just have an assignment of a variable for example then the precondition has something to say and then the post condition is there's a new variable and it has the new the value that you assigned it to um and similar for if statements these are all relatively easy to handle the only interesting part is when you have a while loop because then again this the same code might run many times and it's not so clear what its effect is so there's a template for handling that uh you have a some you have some precondition before the loop and you try to prove some post condition after running the loop and the template says that's not enough you also have to to come up with uh what's called a loop invariant that's a specific specific statement and um it has to satisfy three conditions namely it should be true before the loop so I has to be true here then if you have the invariant and the condition that means you continue another iteration of the Y Loop then the uh invariant has to be re established at the end of the of the

10:33 loop and finally if you have the uh if you have the invariant after the loop then together with the statement that the while loop does not continue must give you the post condition you wanted okay uh let's see a concrete example for this one and maybe that becomes it becomes a bit clearer uh the example is this piece of code it's a simple function that computes the maximum entry in an array of numbers I'm sure most of you would be uh give you five minutes and you coded this up in some language so how would you find the maximum in an array of numbers well you go through you keep a running maximum from the beginning in this case so we have a variable I that goes from through the array from um starting at one and until the end so um I should maybe point out my arrays start at zero that's that's the default and uh I use these square brackets to index elements like in almost all languages and here this function has a precondition namely that n is at least one you're not allowed to call the function with an empty array I guess it makes sense because it's hard in general to return the max maximal element of an empty set it's not

12:01 well defined if it's numbers maybe you can find some Infinity value but let's uh let's um ignore that so we have a a precondition which is this one in this case that's something the program can rely on when you run it and your proof can assume that then how do you find the maximum you keep a current maximum that's uh starting with the first element and then when you itate through the array if the new element is bigger then that's the new running maximum and otherwise you keep the old one right so the code is not very interesting or not very complicated but how can we formally prove that this does the right thing so clearly uh the post condition should be the output what I return here current Max at the end should be the maximum element in this array that's the post condition we want and that's spelled out here in in formulas so uh at this point at the line 13 or after line 13 I want the current maximum variable current current Max to be the largest element in the array and or I hope that's readable for you even if you haven't seen that before it just means uh let k run in this range and then pick the largest um value that

13:25 to get on the right okay so how do we prove this the tricky bit is to find a a loop invariant and I've already done that tricky step for you here so I'll just show you how the final proof works this will not really teach you how to find these proofs but I mostly want you to be able to read them and I just and and recognize if they're

13:53 correct okay uh the loop invariant is is often something you don't find in the first in the first round but you have to refine and and that's the part I've already done for you um there these there these two bits the first one talks about current Max as you would expect and the second one talks about this this I and we'll see where this where this gets uh

14:19 used um do have a well uh I also use this in the template condition that's the that's the condition of the while loop so the that's that's what what is uh what is just copied here to follow the template remember we have to do these three things we have to check that the invariant holds before the loop that together with the condition of the Y Loop in it implies that the invariant is reestablished after the loop and that it gives us the desired post condition at the end these are these three things that we have to prove and so um um let's go through these one by

15:07 one why does the loop invariant hold at the beginning before the loop well uh let's look at the two parts there's the red and the green part um the red part at this point um the important bit here is that I is one because it was just assigned to

15:36 one so current Max at this point is just assigned to a z now if I look at the Loop invariant and I insert what i is namely one then that's the same as this this complicated looking term but if K is just in the range from zero to

16:00 zero that's really all all I'm just saying is it's a z so that's the red part the red part of the loop invariant is satisfied at this point just because it doesn't actually make an interesting statement it just says current Max is a Zer okay and for the green

16:30 part we assume that um n is at least one so if I turn that around it means one is at least n and that means I is at least is at most n sorry one is at most n and that means I is at most n and that's what the loop invariant here says okay so I've proven both parts of the loop invariant of this end statement are true at position a in the code and that was the the first part of the template that we had to do all

17:09 right the more tricky bit is uh part two that's um inside the loop where actually something happens so I tried to keep this here um on the slide maybe it's a bit small so we have a we have an implication that we have to prove and in this case we can we can basically do a direct proof but we'll use a a case distinction because um in the loop body there's this if statement so it makes sense to make a case distinction based on that

17:57 one and it's basically the condition of the if so and I I guess I should be precise and say in that specific line because variables keep changing their values now there's two cases that can either be true or false this this if

18:23 condition so case a or let's let me spell it out case a is that is true so uh AI is is bigger than the current Max that means we have found a new maximum

18:57 um let me copy it okay so that's that's all we know so far but now we have to use the fact that the invariant is true remember we are we're allowed to use in this case we're doing a direct proof so we assume what's on the left of the implication and try to Pro what's on the right in particular that means we can use our Loop invariant and from the red part of the loop

19:28 invariant we can use this bit um now in this case I has some value that we don't know so we'll we'll have to leave it invariant and now I'm just copying what's on the previous previous slide so K between Z and IUS

20:05 all right now now we have to use that we know what the if statement will do because we're in the true case we will execute this line nine and update current Max so in

20:22 uh in this line we Chang the value of uh that means current Max now is AI but that is nothing but the maximum up to the next position because we know from from this

20:59 part that the last entry is the largest so I can go from K between zero and including I and I know the maximum will actually be the last element which is which is AI all right uh so far so good but this is not what the invariance says the the invariant should have the I minus one again so this doesn't seem like we make progress but then if we look at the next line in code we are now changing the value of

21:45 I and so uh after that now I'm sick and tired of uh writing this all the time let me just copy it now current Max is still the same but I've up updated I so if I want that to be the same I have to do the IUS one again right I've just taken this term and replaced replaced I by I + one so I have to do the uh inverse in in

22:16 here well and uh that is the red part of our invariant down that's the red part of the loop invariant reestablished in this case we're still in case a okay I'll try to get the indentation

23:06 right case b is the false case which means and now I should be able to copy some bits if it's not greater then it's less or current Max by the loop invariant still is this almost a

23:41 bit it's almost indicating we're doing too much copying so that's that's still true because it only uses the loop invariant but now uh because AI is smaller than this maximum in the previous range

23:59 I know this is actually the same so that uses uses this condition I should also do it in blue again that means that's actually the same than uh letting K go one

24:19 further now in both cases we arrived at this statement that uh current Max is the max of the first the uh positions up to including I but for different reasons right in one case we had to do the if and update it in the other case we did not update it but it was still the maximum and then the rest is the same so after line 10 we again change

24:47 I we update I so uh I'll do the same change as and so again the red part of the loopin variant is reestablished at D good so that's almost done but we also need the green part of the loop invariant we also have to show that this is still true and that's that's maybe not trivial because we change I

25:54 again I use too much space so I'll shrink it a bit more hope it's still somewhat legible so at position B the loop invariant was true and so the green part of the loop invariant says I is strictly less than n the only place where we change

26:29 10 let me use the assignment and if I was less than 10 strictly less than 10 before now if I make it one bigger it's still lesser equal n and that's what the what the loop invariant wanted so also the green part is true and note that for the green part we didn't have to do the case distinction the if doesn't change the outcome

26:58 there now that means uh we've proven the second part of the statement it's it's a while ago but uh We've we've established this one now if the loop invariant holds at the beginning of the loop together with the loop condition it holds at the end of the loop body now what's missing is the last part namely that uh we're we're proving the right thing and uh this one will be short I

27:33 um can I copy this part have to take a I can take screenshots let's do it that way and what we're trying to proove is this and let's also be lazy and copy the post

28:20 condition so that's my service to you don't have to remember everything it's all on the side so we take our Loop invariance and uh add the the condition of the Y Loop negated that condition was that so if I take I and negate the condition what I get is is the loop invariant and the negation of

29:09 n now if you if you look at the green part of the invariant that means I should be less than n and greater less or equal n and greater equal n so I is equal to n

29:26 right and now I take the red part of the loop invariance and uh insert insert I the value of I and so it says current Max is the max 4K in the whole

29:47 range and Tada that's what the post condition was okay so that concludes the the third part we've or can take it off here uh We've proven that if we have the Loop condition after the loop plus the negation of the while condition so that we actually terminate it those two things together imply what we wanted namely current Max is the maximum of the entire array o yeah I know it's tedious right uh this is the level of detail that you need for formal verification um that's the level of detail that a computer can follow a proof and check step by step that it's correct I would have to spell it out in a different language I've used English language to convince you uh and you can formulate it in a logic language for a computer but that's the kind of level of detail where no further doubt is is possible we'll often stop a little higher level than that with a bit more uh abstractions in but I want you to be able to recognize when a proof is formal and at least be able to read them you'll do another two basic examples of that form in the tutorials namely on mathematical induction and on the uh termination proof and hopefully then you have a a at least a feeling for what

31:03 these proofs should look like