Video 0-5: §0.4 Correctness proofs (part 1)

0:00 <Untitled Chapter 1>

0:04 okay as the last little bit um let's briefly apply this to proving some things about programs and algorithms the bigger picture here is there are some applications where you really want uh more confidence in a piece of code than the programmers said yeah it looks good and that's where formal verification can be applied so you you formulate in these kind of statements for all acts exists Y and all these things you formulate what the program should do and then you try to formally prove that we won't do that to the full detail because it gets very tedious and it's quite a topic of its own but we'll touch on two things that are usually necessary for that um correct usually means two things first of all the code actually finishes its job eventually and if it does then it computes the correct result so I'm thinking of systems that have a clear input computation output Behavior they compute some function uh there's other theories about other systems that continuously run and will feel some some purpose uh this is not what we're talking about um in a way the formal verification um we need here is there's something that you assume at the beginning of the program then the program runs and thus does its job and

0:10 Formal verification

1:36 then at the end something should be true so that's precondition and post condition that's what we usually have in mind here so there's some assumptions that the algorithm makes for example the parameters of a function the input value has to be a positive number then the code executes something and that leads to a post condition that hopefully has some value to you we'll see examples

2:23 Proving termination

2:26 for the first bit I just want to briefly touch on how you can do this and we'll do some example in the tutorials then suppose you have some function a procedure in my pseudocode lingo that um that is recursive so it calls itself it could be our towers of a noise solution for example and you want to prove that it eventually stops right a recursive function could keep calling itself the formal way to prove that is to define a potential some quantity that keeps going down but cannot go down indefinitely so the important bit here is that our potential is a natural number a natural number is famously stop at zero there's no way to go further down so if you can somehow prove I should have mentioned the parameters so the potential exactly depends on the parameters to the function say in our Tower of no example you call it with the number of disks that you want to move and probably also where they are so what's the current poll that they lie on and what's the target Pole that's the parameters of the function and then the potential can depend on those parameters what do you try to prove then is whenever the function calls itself recursively like Tower of annoy move

3:53 this there then do the red move and then move it back to the middle in all these cases the potential drops by at least one it strictly goes down and because it's it's a natural number that means it drops by at least one okay so example from towers of Hanoi the potential could just be the number of disks whenever we call ourselves we call ourselves on a stack of disks that's one shorter that proves that we have to finish with this recursive call eventually because we always go one step down so at some point we reach no discs and then the procedure can just return okay

4:37 the idea is more versatile the potential can be more complicated and depend on on the parameters in interesting ways you'll see an example in the tutorials yeah I think that's that's basically all on this potential it's just a convenient way to make make the notion rigorous that's when you recursively call something you should somehow make something smaller you can apply the same trick to a loop instead of a recursive call if you have a while loop might return might never finish but if you can show that some potential function that's defined on the variables of the of the code there goes down in each iteration of the while loop then it must terminate okay

5:31 the second bit this is about uh correctness in the sense of computing the right result if it terminates in this case we'll we'll talk about these pre and post conditions and I picked out the the most interesting case of that um so often pre and post conditions they say something about the values of variables and for simpler statements like if uh if the statement is X is assigned to X plus one increment X by 1. then in if the precondition said something about X you know that what the post condition will be it says the same thing just uh where the value of x is updated so if the precondition was saying X is at least five then the post condition would be X is least six right if we increment X by one these kind of statements there it is easy to go from what what is true before to what can we guarantee after it gets very tricky with loops and that's the example I want to pick out here or for a general Loop a while loop you need to work a little harder so the setup here is we have some position before a loop and we know there's some assumptions we make what is true before the loop then we have a white loop with some

6:51 condition it does something and then we want to guarantee some statement after the loop um I'll have a more concrete example on the next slide um I wonder if we have to push the example to next week though

7:18 let me walk you through the the sequence of steps you have to you have to do in this case uh the the trick here is to find some condition called The Loop invariant for which you can prove a few things you can prove that it is already true before the start of the loop it is true again after the body of the loop but here you can assume that you are in the loop so you can additionally assume the condition of the loop to be true and you also want to be able to prove that the same invariant is true after the loop uh that sounds a bit abstract I guess right uh but that's that's a way um it's a formal strategy whatever I is if you can prove these things then um you can hopefully get some desired post condition let me at least show you the the concrete example

8:18 Loop invariant - Example

8:22 and I think we'll do the the proof applying the principle here we'll do uh next time this is a little innocent function that takes an array and finds the largest value in the array and how would you do this well not too hard you start with some you keep the current value you go through the list and you always store in the variable what's the current largest okay and so current maximum I guess the name suggested holds that current maximum and so initially that's the first element and then we do a loop until we haven't reached the end of the array we check if the current element in the array is bigger than what we previously had as the maximum if so then that should be the maximum at least for now and otherwise we don't change it and so you run through this and you eventually return current Max you probably agree that this code is is super easy and it's quite obvious that it's correct however we've already had obvious code and it wasn't correct so maybe we should be careful in this case it is correct there's no no hidden nastiness but what I want to do is walk you through the precise steps if you need it to show very rigorously that this computes the

9:44 right thing and often along the way we noticed that there are some some Corner cases and site conditions that are easy to miss like calling this function with an empty array is not a good idea right if we access the zero element question

10:22 I can like pick something and show that foreign okay so this yeah I mean the question is maybe a bit two two questions so one is can you automate the proof can you automatically find the proof and can you use that to find the algorithm right

11:05 yeah so it's the tricky bit in this case the part that is not automatically where there is human Insight needed fundamentally is finding the loop invariant there's nothing in the template if you check here this template lists a few things I want this and this and this and this it doesn't tell you how to find the loop invariants and the reason is no one knows a strategy to do that automatically it seems not so easy possible at least not in general um it seems not possible to tell the computer this these are the steps then you have your Loop invariant in some limited case it is it's definitely doable but uh not in general and also what what happened to me when I wrote up this proof I had the first part of the loop invariant and was missing the second and then you notice you you're somehow stuck and you need to add something else to the invariant

11:18 Loop invariants

12:07 um yeah I think we should we should come to a close and I don't think I can do this in one or two minutes so let's postpone the the detailed example for next week