Explore
For Enterprise
Join for Free
Log In

artes y humanidades
Negocios
Ciencias de la Computación
Ciencia de Datos
Tecnología de información
salud
Matemáticas y Lógica
Desarrollo Personal
Ciencias Físicas e Ingeniería
Ciencias sociales
Aprendizaje de un idioma
Grados
Certificados

Explorar todo lo que Coursera tiene para ofrecer

Explorar
Buscar
For Enterprise
Inicia Sesión
Únete de forma gratuita

Invariants

Loading...

Principles of Computing (Part 2)

Universidad Rice

4.8 (271 calificaciones) | 10K estudiantes inscritos

Curso 4 de 7 en Fundamentals of Computing Programa Especializado

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.

Destrezas que aprenderás

Recursion, Algorithms, Python Programming, Tree (Data Structure)

Revisiones

4.8 (271 calificaciones)

5 stars
229 ratings
4 stars
35 ratings
3 stars
7 ratings

AM

Jan 13, 2017

If I wanted to learn programming from scratch, I'd take this specialization. They are great teachers and the recursion section was extremely helpful.

AF

Dec 08, 2017

Another fantastic course from the team at Rice University. The coursework is interesting and challenging, and I really feel I have learned a lot.

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.

The Importance of Modeling 3:04

Assertions 7:22

Invariants13:22

Software Development 14:52

Impartido por:

Scott Rixner
Professor
Joe Warren
Professor
Luay Nakhleh
Associate Professor

Transcripción

[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.

© 2019 Coursera Inc. Todos los derechos reservados.

Descargar en la App Store

Consíguelo en Google Play

Coursera
Acerca de
Liderazgo
Empleo
Catálogo
Certificados
Certificados MasterTrack™
Grados
For Enterprise
For Government

Comunidad
Learners
Partners
Developers
Beta Testers
Translators

Conectar
Blog
Facebook
LinkedIn
Twitter
Instagram
Youtube
Blog de Tecnología

Más
Términos
Privacidad
Ayuda
Accesibilidad
Prensa
Contacto
Directorio
Afiliados