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

0:00 Introduction to correctness

0:03 and that brings me to the last topic of this unit on proof techniques and that's about correctness proofs so in this case we want to show something about programs about algorithms and we want to show that they're correct now what does correct mean

0:24 so i mentioned before that there's a whole a whole field of formal verification that shows that that tries to show that the program computes exactly what is desired it's not our focus here but we will informally use some of the techniques to reason about algorithms because after all an algorithm is not very useful if it computes some some random nonsense we want to be sure that it computes the correct thing before we accept it as a good and efficient algorithm

0:56 for formal verification you have to specify exactly what it means for your program to be correct and that's usually two distinct things first we want to prove that the program eventually terminates so whenever you give it a valid input it should eventually finish now that sounds obvious but a program can run into an infinite loop or an infinite recursion and you might not really know what's going on it's just very slow and it keeps going and you don't know whether it will ever finish or whether it will just well it will take a very long time or it will run forever indefinitely and the second thing is we want that if the program terminates it usually produces some output and we want that to be the the right value that makes a little more sense if we go to a specific problems but that's the the usual two things that we're concerned with now for proving termination

2:00 Proving termination

2:05 i will formulate this here for a recursive procedure so you have some some procedure that calls itself again and it has different parameters and we want to show that at some point this recurs this recursion stops

2:28 a way to do it is to define a potential function that's something intuitively that becomes smaller with each recursive call that's formulated here but i'll come to that in a second and that has to be a natural number that's important and well that's at least zero by definition because a natural numbers is only starting with zero so that's some function you compute based on the parameters that this procedure is called with the second step we have to prove is that whenever we have a recursive call we have to look at the code that implements this function and if there's a recursive call to this same function procedure again it will have some other parameters and they will somehow depend on the initial input and we have to prove that whenever we do a recursive call we get strictly smaller in terms of this potential

3:30 and that means eventually this procedure has to terminate because we can only strictly decrease so that's that means it's um at least well that's that's the same as saying this is less than

3:52 these minus one and we can subtract minus one from a given number that we start with only a finite number of times a similar idea can be made for loops if if you have a while loop instead of a recursive call the two things are actually fairly similar and you will see an example of this in the tutorials where you apply this to a loop to show that it terminates

4:21 Loop invariants

4:24 on the second part proving that the output is correct i want to uh show you one one specific uh technique that often helps for that and that's called a loop invariant so uh here the setup is there's a certain condition that we know that we assume is true before the code runs that could be something like the input is valid our list of numbers we're given a list of numbers and they're all uh integer numbers

5:02 um sorry that's the the precondition that's a that's something that holds before the loop and then the post condition is what we would want to hold after the loop for example it could mean that the input is sorted i will show you a concrete example for this proof but keeping an eye on the time i would probably postpone that to the next session but i'll explain the setup here and then the concrete example will follow so to prove that the post condition holds after the execution of the loop is our goal and we might have a precondition that's true before the loop

5:45 and then there's a certain strategy how you can do this and it basically means you have to look at specific points in the code before the loop and after the loop but also the first thing inside the loop and the last thing at the end of the loop body

6:06 and then you have to find what's called a loop invariant that is a statement a logical statement about the variables in your code that has the following properties the invariant is true at a before we enter the loop the invariant is true

6:31 when we well it's true at a and if we enter the loop then condition the loop condition is also true so at the beginning of the while loop we always have this so we can assume i and the condition hold at b and we want to show that this implies again that the invariant holds at c at the end of the body of the loop and finally if we left the loop we know condition can no longer be true because otherwise we would have jumped into the loop again so at position d we know we want to have that the loop invariant and the negation of the while condition together imply the post condition that we are interested in i realize this is this is fairly abstract and it might be a bit detached from your experience but once we go through the concrete example um i think it will become much clearer and again it's it's just a recipe how you can structure these proofs the creative and tough part is still to find the correct loop invariant