This two-part course introduces the basic mathematical and programming principles that underlie much of Computer Science. Understanding these principles is crucial to the process of creating efficient and well-structured solutions for computational problems. To get hands-on experience working with these concepts, we will use the Python programming language. The main focus of the class will be weekly mini-projects that build upon the mathematical and programming principles that are taught in the class. To keep the class fun and engaging, many of the projects will involve working with strategy-based games. In part 2 of this course, the programming portion of the class will focus on concepts such as recursion, assertions, and invariants. The mathematical portion of the class will focus on searching, sorting, and recursive data structures. Upon completing this course, you will have a solid foundation in the principles of computation and programming. This will prepare you for the next course in the specialization, which will begin to introduce a structured approach to developing and analyzing algorithms. Developing such algorithmic thinking skills will be critical to writing large scale software and solving real world computational problems.
Invariants
Loading...
Del curso dictado por Rice University
Principles of Computing (Part 2)
235 calificaciones
De la lección
Modeling, Assertions, and Invariants
This week, we will explain the importance of modeling. We will also explore how to use assertions and invariants to ensure that our models are always consistent and correct.
Conoce a los instructores
Scott RixnerProfessor
Computer Science
Joe WarrenProfessor
Computer Science
Luay NakhlehAssociate Professor
Computer Science; Biochemistry and Cell Biology
[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]
Explora nuestro catálogo
Inscríbete de manera gratuita y obtén recomendaciones personalizadas, actualizaciones y ofertas.
Coursera brinda acceso universal a la mejor educación del mundo, al asociarse con las mejores universidades y organizaciones, para ofrecer cursos en línea.
© 2018 Coursera Inc. Todos los derechos reservados.
