[MUSIC] Welcome to class. In this lecture, we're going to talk about using logic to reason about your programs. In particular I'll introduce the concept of an invariant. An invariant is a logical condition, that holds repeatedly at certain points during the evaluation of your program. Now, we already have some invariants that, we're aware of in this class. Here's a classical one. Scott wears ties. Now the critical thing to note about this invariant is that it holds, when Scott's shooting a video. It also holds when Scott's at work. But it doesn't have to hold all the time. For example, I'm pretty sure Scott doesn't wear a tie when he's taking a shower. At least I hope not. For invariants for your program it'll be the same thing. And invariant will hold at one point during the program, there'll be some computation, and the variant will hold again. Some more computation, the invariant will hold again. So the critical thing is the invariant doesn't have to hold after every statement, but it has to hold repeatedly as your computation advances toward an answer. We'll look at some examples and some definitions, and I'll show you how we can use invariants to help, basically build better functions and reason about the correctness of your program. An invariant is a logical condition that repeatedly holds during the execution of your program. So here, just a logical condition you can just think of, is a Boolean expression that involves the variables on your program. I'm going to use invariant of something to be this, represent this expression for these notes. So. This condition should hold as your program executes. And in fact, if we kind of label the points where it holds P1, P2, up to PN. Then we can actually kind of, express relationship between the condition and the portions of the, the execution trays for your program in the following way. So if I let fragment_i correspond to the portions of the trace. Between the points Pi and Pi plus 1, then we can split the trace of the program up into pieces, and then kind of add assertions that reflect the fact that the invariant has to be true. So here are the fragments. Fragment_0, fragment_1, fragment_2, up to fragment_n. Those are the parts of the trace. What we've done is we've added, assertions here that say that the invariant is true between these fragments. So what you can see, here it is, let's run some code, check the assertion, check the invariant, run some code, check the invariant, run the code, check the invariant. So we're seeing that the invariant is true at multiple points during the execution of the program. Now you're probably asking, well why the heck are we bothering with this? What does it do? Well. A well designed invariant can help us do two things. It can guide us in building pieces of our program. It can also help us verify that our program's actually doing what we expect. I mean notice here for example. If I know the invariant, if you give it to me. I know when I write this piece of code for fragment_0 that, it has to actually guarantee the invariant holds after we execute fragment_0. Let's think about how we would actually build fragment_1. Fragment_1 can rely on the fact that the invariant is true, whenever we begin ex, executing fragment_1. And then we have to make sure that after we finish executing fragment_1 the invariant is true again. So this gives us insight into how to design these fragments of code. The other thing is that it allows us to reason about the correctness of the program. Kind of reasoning about all these invariants at once is difficult. But notice we've kind of isolated it down to pairs of consecutive invariants, okay. If we assume that the invariant is true, say, before we start executing fragment_i, we can use that fact when we're actually executing fragment_i to then try to derive the invariant is true after execution of fragment_i. So we can chain all these assertions together to reason about the entire program. That'll be very valuable. All right, the previous description was fairly abstract, so let's get our, get our hands dirty and look at a really concrete example. So I'm going to talk about invariants for loops. So, the idea is that we're going to build an invariant that's going to help guide us. In both writing the code for a loop, and then verifying that the loop produces a correct answer. So here I've got a function, it computes the factorial function. It's kind of our favorite test function, and we've actually already designed an invariant for it. So we're going to have a local variable answer and a local vari, variable index and we want to make sure that our invariant is, the answer always holds factorial of index. So, couple of things to note here. This invariant doesn't hold after every statement is executed. It only holds where it actually put these assert statements. Okay. We talked about code fragments up here. So when we're evaluating this function iterative factorial. Kind of the first code fragment is, we said answer to be one and index to be zero. So we now like for this invariant to be true. The invariant that answer is equal to factorial of index. Well let's see. Is one equal to factorial of zero? Yes, it is. So good, we've made sure that the invariant holds now before we start trying to execute this while loop. So now, what's the next fragment of code we're going to execute? We're really going to execute the body of this while loop. We're going to repeatedly execute the fragment of code that corresponds to. We increment the index. And we take the answer and multiply it by the new index. So what we'd like to do is if we start off before we execute the body and we know this is true, we'd like to then verify that the invariant holds after we execute the body of the loop. And so the thing to note here is. That, before we execute answers equal to factorial of index. We now increment index by one. We make it one larger. So what do we need to do to this running product that we're computing for the factorial? We better multiply it by this new value for index. So if we do that, we're guaranteed now that the new answer, again, contains the updated factorial. The final thing to note here is that this factorial that allows us to reason about the correctness of this loop. When does this loop terminate? The loop terminates when index is equal to num. So if index is equal to num, then we conclude that the answer is just math.factorial of num. Our loop actually correctly computed factorial. All right, let's look at this function inside Code Sculpt. So here's my iterative version of factorial. We have two assert statements, that contain our invariant. And if we run that, sure enough, it says the four factorial is 24. That's awesome. Now, I talked about the interplay between building these fragments of code and checking that the invariant is true. Lemme show you an example of how this can help. Let's say I was writing my initialization for my loop, and I made a silly error. I initialized answer to be zero. As I run this, the invariant, is violated immediately before entry on the loop, in particular zero was not equal to zero factorial. We could also use this to check to make sure that the body of our loop is doing what we expect. Let's run this and maybe have it do a sum instead of do a product. And sure enough again, we get an error here that says we violated some variant. So even if you're really not reasoning about your programming you can use, the invariant to check to make sure that the code you've written is doing what you intended. Let's go on down and I'll show you a few more examples in this file here's one where I've annotated merged with an invariant, the invariant is the answer. Is sorted. Notice it's actually, we're asserting this at various places during the program. I've actually gone through and annotated two recursive functions with an invariant. In this case the, basically the recursion is computing the, correct value for factorial. Down here have an invariant that merge sort is returning a sorted answer. So again I'm really not doing, m, a lot of reasoning here but I'm just going through and adding invariants in to check that my computation is proceeding the way that I had expected. Okay, let's look at one more example and I'll go back to the notes where I'll talk a little bit about how we can use invariants inside classes. Now let's talk about how an invariants can apply when we're building classes. So. If you recall back when we worked on breadth first search, we had a wildfire demo that kind of explained breadth first search in terms of a fire spreading. In the class that I built for this wildfire demo, the objects that I built had both, a boundary queue. And a grid. And the boundary queue was designed to kind of model the boundary of the fires that burned. And, during the use of that class, I always maintain the following invariant. And when we, ever we added a cell to the boundary queue, we always set the corresponding cell in the grid to be full. That kept us from adding that cell back into boundary queue a second time. So that was actually an invariant. I never actually explicitly formulated or tested that are anything like that, but we can actually update our implementation of the wildfire class to actually explicitly capture that invariant. Now the condition that were going to build is going to be complicated because it’s going to involve all the cells in the boundary queue. So in that particular case, you may not be able to write a single expression, but we can actually build a method that captures that invariant. So here's a method called boundary_invariant. It takes all the cells in the fire's boundary and then checks to see if that cell is empty. If it's empty, we've violated the invariant. So what we do is, we print out a message to say something went wrong, and then we return false. If all the cells are full, then everything's good, we return back true. So, this method now actually captures the invariant for our wildfire class. So let's go look at the code for a little bit. All right. Let's finish off class, and look at a slightly modified definition for the wildfire demo. Here's the class definition. If I scroll down to the bottom, you can see probably the two most important methods. This is update_boundary. This did one step of breadth first search. And this method boundary_invariant checks to make sure that, every cell on the fire's boundary, is also set to be full. It takes one that's empty it prints out an error message and returns false. So I've gone through and I've actually added that invariant to update_boundry. I want to check and make sure that this is true. And in fact you can see that I kind of guarantee it's true, by just having two statements here. Th, if I add anything to the fire's boundary I go through and also set the corresponding grid cell to be full. We could run this, and it's all good. I'll start doing some DFS, and no problem. Just double-check and make sure that it's actually doing what we expect. Let's go through and actually just comment out, the statement that sets the corresponding grid cell to be full. So if I run that. Sure enough, I get an assertion error here. I added something to the boundary. And the corresponding cell was empty. now, this leads to kind of an interesting observation. As I thought about this example. I was thinking, is my class definition always guaranteed to make this invariant true? Let's scroll up, cause I think I have a method called in queue boundary. And that just lets me throw something into the boundary_queue. Now in the version that I had for my initial implementation this was all there was. What happened was when I called this an update, update_boundary or inside the gooey I always did a corresponding set full for that grid cell. In other words, I relied on the user to make sure that the invariant always held. Probably a better design would be to just design a class so that the invariant is always true. Don't rely on the user, the user's going to screw up. Just, if it's an invariant, make sure it's true. So here's what I've done, I've gone through and I've set the corresponding cell to be full, and then I've asserted the boundary_invariant again. So. This version of the class now has the property that I can't violate it by doing in cube boundary. Now I could still violate it by doing, say, maybe set empty for one of the grid cells. So I need to consider that also. But the thing here is not whether this is correct or incorrect, it's the fact that by formally expressing an invariant for the class, it made me think about how I built my class methods. And so it exposed some of the corner cases that might trip me up whenever I'm trying to either debug the class or when I have a user who hasn't really talked to me a lot, use the class. So the, the upside is here that, by thinking about invariants in a more formal manner, you can improve the quality of the code that you're writing. [BLANK_AUDIO]
