00:38
I did not expect that he's put they're working. Oh I didn't know that. I didn't try again. Is there any caving? Because I think it's more like maybe or there was

02:14
All.

02:19
Is CS5 under 50. There is some power problem product and the loop

02:32
So we starting to do that but the professors of things that's saying that lets us sign. One day trying to terminate that well yeah.

03:24
And like the desire.

03:43
Hopefully, we should have nothing still contract is only one.

04:08
Campuses business like, parameter.

04:57
It's not really every.

05:22
Department decided to have a faculty meeting outside in the shade. I was shivering the whole time.

05:38
Until it when you deliver morning? Yeah, that's is accents because

05:50
Was talking to a colleague at Austin. She was saying that yesterday was a hundred degrees. It was.

06:01
It's all the only and I get so gladly.

06:26
Anthony can tell completely during the the most for you guys. Feel stressed. You guys will stress stress. You will have the ability to build strikes, I mean, I guess someone questions,

07:02
And let's first start is the homework, we next week. So we did an exercise in class, in terms, marketing chair, and specification program and verification over of the system that supported the design to meet that particular barrier. Thank you. So, this is the mental homework is really in some sense.

07:28
Similar. Obviously some differences. So again, you're going to have to do it on processor design.

07:42
Kind of view your first section, then you're going to have to do a form of specification.

07:56
Then you're going to have to do the program, and then you can do it verification, but you don't need to verify the whole thing. Only the, the products.

08:17
And so, what this means means means that you have to develop a metric and each then you find the progress, develop the metric. And then, inform informally argue that, you know, the symmetric decreases and keep on the reach. The final state. The in process of doing that, you may need to refuge variance by the focus is on the progress.

08:50
So what is the problem? Have a pipeline of processors? It's a synchronous pipeline.

09:16
And that same plus one processors.

09:34
These prices are as to registers in the and what's happening. Is that basically it's it's like a big shift kind of register where hey, goes into be legos this way that way. That way comes back and back. So your circulating times between the soil, the bean registers move this way.

10:07
And then at the end, you drop it. Here's to be convenient so that there's nothing else happens. You just run the numbers in a certain way. Okay, okay. Now, there are two kinds of values that are being done in a number of the greater than zero. So they don't integers so you can bring them to you.

10:37
And then basically that means it's big and then and can be equal to zero. I should not use an let's say x kind of next and that basic is that

10:55
So there means it is real processing is data. Some of it is not really needed it's because it's not. And if you do close enough,

11:14
So we're using a lot of power we close. We have processing garbage, attention data now. So what we want to do the basically we want to use on as many processors as we actually need. So you want to eliminate the garbage. So that's why I saw the zero animation.

11:33
So, these is going to be the, at least, at least more.

11:52
Devices are disciplination, at least.

12:06
And that's to make the programming easier in the coding easier, okay? So, what do we want to do? Is the data circulating. We basically, we want to accumulate the zeros at the end and we get two zeroes here. We know that this processor is not only here so it's shut it out.

12:34
And then so this is no longer the last process. So the next one is the last and so on because we have at least four non-zero means that you always gotta have at least two processors. So all kind of special cases are eliminated that special case, what, you only have two values and you have to circulate them with the same thing and all kind of, you know, what, you don't have the the first and the last processors to active are the same processor.

13:03
So you need all those cases. So, the first process is always the first processor, and there's always a last processor, which is different from the first process, okay? So if that 4 zeros, we're going to eliminate the process of the end. If there are five zeros, you can make only two processes at the end and one zero.

13:26
Just keep it are always be too to some number zeroes. Well, that n plus 1 processor. So that 12 plus the numbers.

13:44
And more than four are non-zero By yeah. So if that's really up like have the when we when we see zero zero, the processor is no longer needed. But when there's zero number, they did not number of zeros. Yeah. Into. I mean and zero is going to still stick around, can contact eliminated but maybe there's some way to not just circulating.

14:20
Now you the numbers, I'm not changing because you're just looking through. But this would be an example of something, you actually would work with real world values. So for instance, we you know, the they can be even in outward. So the values that we are and they could be processing of the values so that that is actually computed.

14:45
They dice it out, can be all kind of processing but we are not warning about that though. We can now put no processing but basically just our job is to design the system creating nature to shut down processes. That it doesn't because this way also speed up operation. So it's 20 plus ones steps to recycle and only have four zero four nonzeroes the later speed up and that questions here.

15:22
So the zeros have to be next to each other in order to be zero seven spread out, but it was the only, oh, only 2520 anywhere, it's no one process one. Oh, so I said I have to somehow capture the zeros. Oh, right? Yes, towards the end. So I can shut down the process and you cannot only shut down the process at the end or pipeline.

15:58
It has to run like this. So if you don't even shut down one in the middle, you still have to pass the data through. So there's not benefit or he pays the same number of steps to complete a site, but if you can only shop down the processor at the end, that means you can only zeroes that are next to each other.

16:21
I'm seeing zeroes. Do not have to be next to each other. Oh, you have to eliminate them even though they are not next features. Oh, it can be spread anywhere. Oh. So basically think of it as you know we're running through and you give when you give had me a zero I can hang on to it.

16:41
Oh and then we have me the second zero said well I'll go I'm going home for a beer because I'm done. My work is done that's kind of it the way everything about it. Oh, just can use processors for more than one round. Like you see it? Had he like houses that work.

17:02
So like, give us real estate a zero and a seven. And it's too like, Well, let's make a process starting to

17:25
Okay, so we have a, we have here, we have a seven here, the three here, the two here and the one here. So what's going to happen In one single step? Synchronous one, the seven moves here, the symbols over there, the value comes from here. And here the two moves here that are there in a single thing, but can you have a three jump over a zero or the, you know, you've kind of jumped over?

18:00
I mean what do you mean? Like saying you have he zero? Okay, let's say I have a zero here. We want to keep the we want between zero to stay there, but the data in the port to go, I had to do that. I've been able to still go through steps because that's not the good idea.

18:26
You should circulate the zero to get to the end and trap the dead that's been for the same problem because you get the zeros the end if the order still exactly the same but there might be a one behind it. Yes. Now, how do you so you may have to.

18:47
I mean the last processor may need to know that is the last processor and act in a way, which says I got a zero. I have a hangover. So basically, logically pulls it out of the primary get observations absolutely correct. Now the first problem they drive is supposed to solve is to propose an architecture.

19:14
Now, you look at this and you say, well, you already gave me that today. No, this is a sketch. There's a way since I'm explaining to you how things work. You need to design the across the source, he just given to you. I mean you don't have a choice, you can't change this piece of the design that it has two registers and being so the processor has this students, okay.

19:43
But they may be additional stuff to I mean remember an architecture involves memories in the process and also involves access rights. So, you know, the way the processors took to each other is very important. So if you know, if you have a line from this to that some other architecture and you and what does this line actually mean?

20:25
So, these are registered X inside again. Why this means that the processor would finding this as taxes read access to x, right? Not just,

20:42
So, you know, so that those have to be the access, right? Have to be also identified in the picture if you need additional, you know, additional registers. Also, they have to be identif. So that's one thing. So, so this is not a complete pictures. Basic tells you, this isn't the channel approach but uniquely the details, you need to identify all the registers to show you.

21:10
These arrows that identify access rights. So if it's a sleep, it's a source. That means that you read, if the destination, that means that you write. Okay, so I know he's ridiculous in the same consider. They can write a really to each other, then they just that cannot write or read their memory.

21:34
Pases. Okay. So the processor can read and write to register them, you know, same city, you're not generally, the general rule. Is that the processor those? They don't like them free. That's a general rule But we don't have to write and we really could only do, okay? But in principle here, we can write every three.

21:56
So, but the question, the more complicated issues that what about between processors, you know, which processor has access to what that's part of the design. So, you could say for yourself, I could put a line from here and here and this line would say, so this is let's say this process of n plus 1 and this is possible 1.

22:27
Okay, if I add that line there and by the way, let me just be very careful here. See the line touches here and touches there. That line says, in plain English, I process a number one, swearing in front of the judges that I have allowed to read from register to be a customer and plus one.

22:50
That's what it says or you put a line like that, okay? So, if you need to be able to reach from another processor, then you have to draw the proper lines. Clearly, if you are shifting this way, this process or cannot get this number, if it doesn't the right surprise or he pays the percentage here and he writes to the desperate story right there, thanks to have access rights to right there based on these secondary by.

23:31
This is the one this time. So, do we need to keep some zeros there with one there? Keep this beer there. You want to capture the zeros at the end? Yeah, you come to the garbage. And when you have enough garbage, then you process it. If you like the only one, the other here.

23:52
So it's only one. Yeah, we need based on the specification. Here we needed. Little rock. Now, you don't need to live. You can trap it at the end and just circulate. Okay, so it's very important for the, for the processors to be uniform. So, they look alike the act alike, and his own view as many special case.

24:31
So that's very important, it's all so you don't believe. Build one process sword that he has five registers and one price on that is three. You want the same mask, the same design, simple business being chips. So you got the row and you on a bus and you go the same team, so if you can the last one and then all the others are just can be on the same, you know, them simply, that's the best.

25:01
Now, obviously, I'm gonna have to be different because you see it was different than right. It does. Some different kind of work. So this is special but the rest of the trips to the identical here, the code should be the same. Yeah, the other thing part of the implant one processor, it's a little bit different from the, you know, not be.

25:26
That's a part of the the design guideline make it look exactly the same. So when you look at a jet, you should be able to take this one and this one has swapped them and the processing should be stupid. Still the same. Okay. But that's part of the design that you need to go to think, again, send me the design, get some feedback on it.

25:49
If some customers in this room, I'm not gonna name names. The basically submitted there. They're a homework. Who's only one question on the feedback, you know, and the line and the last moment on, you know, Tuesday night, you need to get more help and others. You know, we know we have these changes back and forth and we got frustrated with each other and so on.

26:17
But we all learned I don't from your from your frustrations, I don't how you're thinking and then you know what, what's difficult it seems like that so you know, we all learn from each other. That's why we have that interactions. My mom, my wife is not, no problem. We're supposed to be doing something else.

26:38
It's a, you know, I need to take care of my students. That's my first violin. Yes, I have one. So the final processor could, it can be the vegan. You're there could be right to be can never write because of anything. The processor write the to arrow the right arrows.

27:06
He could that'll be done.

27:12
Because means that they communications fabric between the chips changes based on location. So, you soon do that and I'm sure that we're gonna come up with that design. And I'm gonna tell you don't do that because if you want to keep it simply. So for instance if this processor is the one that is from here.

27:34
Well, I was thinking about zero than you would be. Well, not in the zeros and non-zeroes, okay? If this processor treats from here and then you want to read from there, that's not a good design, always. So the arrow pointing this way. Isn't a how don't this since you're not a pipe.

27:56
Okay, it's just, you know. Let's think this notice when I stop the arrow, the arrow stops not where the data is going. But the the perspectives who has a right to read the data is the processor that has a right to the data. And it can do any civic ones If could have 10 different high speed registers here that it does something with the data and then and then I don't care.

28:26
Okay. It, but this is the denial that we can be. So this is memory and this is rights. So these process was at the right to read from and have to make sure that you're done next equations. What two processors? Write to the same cell because that's going to be a conflict.

28:47
It's always easier to read from someone than to write to someone in. When you're writing surgery it's always easier to just read the output lines rather than you know, writing side someone else. So keep in mind all those things, it doesn't have power because you get. Yeah, it's impacted the town.

29:11
If you want to join the circulate and there is behavior is totally different from the, the one in the middle. Yeah. How do I define to differentiate the importance of the behavior of Google? Okay. So one example you said let's say that this is I build a the chick that can you know can rotate data like this or like this and I want to write only one one.

29:44
I mean people only want basketball one chick. Well, I can set the bit and the bit says rotate left. And what's rotted, right? So, I get both behaviors in a single chip and all the change will define

30:03
And then when you get to to write a code, you have to be very careful to kind of know. Not to hide the type of the, to highlight the fact that this chips are really the same and I mean the same code, it should be very obvious that I don't need the same.

30:21
So you're going to do something like, you know, when I do something like this, I

30:35
And then the code for processor. I and that's called is going to be the same lines of curved because I just want to press. All right. Now for one maybe different. So we may need to do this and put one separate. And by the way, obviously in synchronous I need to do so it could be something like this.

31:02
Here it is processor one, but maybe I can combine.

31:12
Another thing that will be careful is that Don't write code, which says if I'm process or number three, I'm going to skip three cycles. What are you know that you're frustrated number three because I'll take the chip and move it in slot. Eight. How do you know that you are free?

31:36
So that difficulties here but if you need to define the behavior of the health and selling behavior, but for some situations they want to have different data driven. Yeah, if you, if you get the negative number, you say it's an exception. So you stop over five line. So yeah.

31:59
Okay, it's a fun. It's a fun thing in trying to keep it simple and like it's a uniformity of the processors as the best is it. You can really do it like this, so it doesn't, you know, it looks so all alike.

32:25
And you know that we talked about schemas before it's a the pattern that I just showed you. That's a schema you based on the eye. The code here is translated for that. I goes on to the ice processor. So it's i3 you put on the place. I was three and take this code and put on the third process.

32:55
So clearly I mean the very careful about access rights. Who is allowed to lead to from what and be careful making very uniforms. So every single hour and you're gonna need, you are going to need some additional information to be able to make this important decisions. So, you may need to have some additional registers and make sure that you keep that number.

33:27
All right, So elevator, let's let's work our way I want us to watch a discussions. Okay. So I'd like I write my solution but we wanted to talk about the implications of what they're like because I mean have mistakes here and if I do I love you too, discover them.

33:54
But I think that you can see the difficulty of when. So the really first point of difficulty is having an our mind English playing in English, a good precise thinking about what we want to do that. Then the next thing is that using the notation to capture the thingy and since it's one piece of the time sometimes it's easier because you know, it's just very melody focused, The most difficult part is to then look at the whole thing as a system and it's very good.

34:37
So if it takes specifications free, how do we improve? The specifications three actress and environment of true. I mean that's what they need to do. And it's not, you know, it's not not easy. And the last thing is that you need to, you know, notation stuff to make the, you know, beating the respect easier.

35:03
So you're gonna make in steps, but you really think of somebody else, it doesn't see it. You know. How did you think about? Okay. So let's

35:17
So first we had to ask it.

35:29
So people variables that capture the state of the system, And we are modeling this system. Like if you're writing a simulator, you know, you're gonna have right cut and you don't go, you're gonna have very good variables, are gonna be present our properties of this of the object are similar.

35:47
It's exactly the same. So we I mean everybody is different technology. So I'm going to use what so we have company. So, for the cabin,

36:05
And it's the world and I think that if you want to, you can have cabbing start as a definition, it will not have been moved and that might be easier to read education. Then it's a member of the style and then they have any locations.

36:40
It's an integer range.

36:48
And copy direction.

36:54
In a second and the militation. So some of you use my notation or as a movement and put in parentheses some of you just use parentheses. So because you know what? The notation. But I have none and there is a this is what elevators actually do. I mean, they have a direction and when I want to elevate arrives, you can see the light blinking dances is going up and it's going down and it's not it's not going anything.

37:30
You don't see any up and down some candy. So this is more flexible by having none. As one of the, some of you basically I'm just worked with up and down and then they have come in coming door, open

37:53
At the end and then you're gonna have a quote

38:11
This is easier to we had floor door open.

38:31
And that.

38:36
Come on to him over. And again, if you want to, you can have

38:52
Okay, equal more more.

39:02
Now, you're gonna see why am I buzzing? Driving. God is, this is a declaration. It's a definition. So you need the part of the pilot of K here in order for this definition to make sense. It King does not appear in the definition. I'm writing it down because some of, you know, very messed up this celebrations.

39:28
So you can stay here, which doesn't make any sense. Whether you're playing an array to put an index on the name of the array, then we have the buttons. So nothing request, okay. It's already one hand and we have outdoor. You don't go and they're the same. And some of you found it in your school, we have a definition called a request.

40:19
Request. He says it is a request for 4K. People tropical okay or not pressing in my notes. I have to spell down out.

40:48
For having.

40:55
But that's again, it's a definition. So these are useful definition and then have the other aspect of just a fight a lot more.

41:14
So you can have the all right? And then,

41:30
So here this is in the basic state and then if you have what are the observant definitions to help.

41:41
At some point, I'm going to raise. Oh, so specification number two, number one, and two other ways to just keep the activity of two. So, the first thing we have saved,

41:57
Generally, safety requirements from a tenure point of view. I mean, from the logic mathematical point of view, that safety, actually, actually safety properties. Like, your guidance. And unless I see better and versus progress problems. So first, we want them, the company's moving, the one, the door could be. So everybody that the valued,

42:32
Implies and in this first part everyone with everybody got it so it's I know it's not much alone most ADP but they need to get the number six.

42:52
So we have the common vote because we find here so we have fun And then dancing is that if the floor the floor that is open even only if the elevator is there doesn't move and there's a lot of. So, the secondary idea running was Lord. All right. He said, only if

43:31
The, and

43:40
Okay. And,

43:55
So that says that if the door is open on the floor, this has to be true. And if this is true that there is over the foot. So if not only and this kind of nice because if you want to say the floor, door is open and the cabinet stuff and the cabins location escape and they can't.

44:25
Because by just saying this, it implies all of that really short and specific, okay? Now, I want to point out many of you, keep them forgetting and dropping their IMDb for the guy. Well, if you mean, I'm very happy to write that. So now many of you is also added here, I will put on the other and the guardians that is not called on n and there's not

45:11
So this is some of you actually defined our outcome and downfall as a ray, from two to n. And from one to n, minus one, that's kind of messy, this logical specification to care of that. Those calls can never happen. So we don't have to. It's clean. It's not really fun.

45:32
We got every single one grand here that together. Now So this is saying then we have seems to be over fire that they need to address. So what happens First of all, when a fire will now be thinking? When a firearm allows yourself goes on, he says you've turned off attorney goes off which options, right?

46:04
So anyway, when if I two years, how old the bottom side is? Set are clear. So that's a very important thing and so we so let's write it down and then just talk about it again. Five on implies not outcome. Okay.

46:39
Call okay, or guardian.

46:49
Now, since studying for a second it says, many of you have sent question about it. The implications of what we just learned. This has to be true all the time which means that, as soon as the final lamp it's on the bubbles have to be open. No, one of the difficulties of modeling, some of these systems is a traditional have any notion of time.

47:17
So I have to very careful to do same that not dependent on time. So, you know, one of you had two seconds delay on the door. You can have to set it there and the door, but then we have to basically model it as multiple states. In the we arrive at the door.

47:36
We wait at the door. We leave the doors open multiple steps and then that chooses that two second waiting at the door, is not going to be just an arbitrary amount of time actually takes three hours in the simulation, but it's placeholder for time. So afterwards, here it doesn't app.

47:58
Call here product enabled or just return return. The request to the what this? So basically, this has in English, is that when the fire is triggered, it causes buttons and turnover called. That's what it says For this long as a file is in the street of state on the final Amazon nobody inside program.

48:30
But actually can be on If they were on before. Obviously, this implies that the action that we, that turned on, that line instantaneously in the same moment, turns off all the problems and enter the carefully. That doesn't make any funny implications as a part of the space. But that's what an invariant system because this is the same state.

48:56
It's not like,

49:03
It's difficult to say, actually that I turn on the line fire alarm and at two seconds later, I turn off the buttons because then the way I'll have to model it as I turn on the parallel, on that move, that implies that we are now into the reset buttons state.

49:25
And then if you are the recent button, state we are required to reset the buttons. So it's very messy. Great company. But by basically saying that here's something. So essentially this is true, this had to so delete. You ensure data case in range of the one children. Because number one, this is for okay, see case prevail.

49:57
So this is for all games. So it's the one two switch. Again, you could also write it for all and for all K, within 1 and N, but it's implied and makes a specific. Okay. Now, what does we want to happen on the fire? Alarm goes, we want to create an elevator all the way to the bottom floor.

50:29
Open the doors and stated. Now in a real specification would have to have allowed for the firemen to come in. Use a different mode of operation and so on but we are not doing public. So to just say that we then we say fire alarm.

50:56
Here.

51:04
Floor company on one again. Direction. Notice how short respect comes. Why? Because Florida often for one implies cabinet. Stop having an location is one and having us a door. So we don't have to copy all that because this is our That's why it's important to write this invalidian first.

51:40
So you don't treat the reader and saying that this is incomplete spends. 10 minutes. Explain to you why it's incomplete and then goes to the next pages. Oh, so sorry. And you could go and, you know, erase everything there. Okay. So you have to put any order to them to help them, tell them.

51:59
Okay, most of you got this but before events, we have to look at the implication of what this says, it says that the final is on. So, in that statement is all, if he's got a continue to be on home away up to the time, elevator at the bottom floor and it wasn't coming that says that, once you turn on the final life, you cannot reset it.

52:37
Such time, the element will get to the bottom of one. Now, that's not the case. The specification is different and it's much more complicated would have to deal with the fact that it could be reset. All the way down and giving vacations. Okay? So again we have to be very careful.

53:02
I mean we are trying it's when I call some environment, right? So we're trying to make some simple elegant so we can understand them, we can reason about dinosaurs. But if this was an how to estimate the first draft will take about two weeks and would have major problems.

53:24
So the significant level And that's why this problem was using internationally as a sample test for specification languages because it's a fear to be simple. But then when you get to know the details, No and something else that's missing me.

53:59
Don't know how to gonna stay in mistake.

54:12
So we say at this state you continue unless the final answer. So see. Okay, let's write it down and let's talk about. So so that would be the fire alarm on again. Floor.

54:45
One coming election. Unless,

55:04
So you see unless he says that if we're in this state normally each other, the only next state which can go to is one of the largest. So that basically says, you can get out of this state by turning off the fire alarm, good. I know it is for instance, that this is an unless is not an key.

55:32
If I don't until will be requirement for the final line to be turned off by being around less, I'm saying that that's the only thing that can happen. Legally. But I'm not requiring you to release, so you have. So that's a big difference. You cannot tell another because basically constraining what the next paper is going to be without just saying, we have to go because we don't control the problem.

56:09
Somebody else is gonna have one person, he said, and and change about. So those are the issues on the of the fire and then he had service. And so we had cabin pay quest, okay? Until?

56:41
Floor door open. Okay. And,

56:56
Okay, or

57:07
Again we hear we have an untill can some of you a couple of times and messages asking about. You can please clarify and the different events tell them at least if you have a leash to here, basically that says that you present after the question. But and sometime in the future, you are going to service.

57:31
And that time request may log you on anymore and the time of service in the future will be resulting in this program. So that's that is one. That's a fundamental difference. See the so the ideal the person has a less part. It says this is going to stay on.

57:52
This state is going to stay on up to the point where this is established. So means that you can't reset the cabinet request without a service again. Unless it is in the fire alarm which is considered another way of service synthetic and you notice on the final arm goes on because of this education here, the surface request is recent.

58:17
So both if you go into this state we're going to this state. The service request is. He said, because it was so,

58:30
Questions.

58:37
Is not coloring good, right? Is not. So we basically said for that, meaning negative force and I'm setting no longer a request. Being named is no longer a request because he service them. So if you don't have this with some of it did not have, that would basically would allow for cabin requests.

59:17
I mean a liberty set in the country which means that once you press the button from four, three that Boston stays on for them. So you have to always go to Florida. Saying if you don't, if you don't have this because it's the body is never, except is not necessary to ask in direction.

59:42
No findings for the request but the cabinet request is not necessarily at the direction because if I press a three, the next times you enter, you will go to three for the down calling uphole. You need to have the directions selection helpful.

1:00:14
The same floor.

1:00:20
Okay, and not out of all and direction combination.

1:00:39
Or.

1:00:48
And this is the same.

1:00:55
So I see here, the direction is important because you should be servicing alcohols if they're going down party from moving their own. Which,

1:01:07
So we end up basically the specification means not that but that season in a high level, we want to be very abstract. So you don't start this opening and closing the doors in a high level. And moving from one floor to another and in both details. So three six nine formulas for the entire spectrum.

1:01:32
It's easy because they have a small. Number of formulas is unique. Understand has look at the

1:01:42
Questions on this.

1:02:10
Who was restated the request. What do you mean you can figure and write you a set? But we need to divide anything longer so we don't know. In fact, well, it's no longer true that's very first case. It's a variable, which is called so true. These were saying that if you start to be true, it ends up for

1:02:46
Cold. If you reset. And the floors are your tablet. Those are open the window. Yeah, those are not open are not afford until you directory, okay? No right here.

1:03:14
Of the period, right? So when you're on the floor, the direction of that Once you arrive and reserve is a request direction. But if you don't know no you doesn't know that it stops. But it's not because floor open door implies that the stop. So we know that I stop to the floor.

1:03:39
Again, if I'm more than a more refined model with separate arrival at the floor, staying in the floor and living with them and being blue floors. Somebody actually did between floors which at this level of specification doesn't make sense to get them.

1:04:05
Notice that there are so progress condition here. So here.

1:04:18
So this side requirements to do something. Why actually have to move the cabin. So in specifications three, what we actually should be doing is replacing this for formulas, was an entire new package of formulas and then showed that the new package accomplishes. Exactly. That's what the refinement means. So, we have to look at us tomorrow and show that, you know, from those we can prove this.

1:04:54
So, and that's, you know, that was a difficult part of the assignment and it's a lot of details. So I know where approaches world, I looked at the motion The problem I wanted Calvin to the way this notifications here. Doesn't control at all how to cut yours. So, he totally possible for the camping to teleport itself, from floor, 1, to 12.

1:05:28
And then to five. And then tonight we don't care what you're not imposing illustration. We just said, eventually you have to come in and services called, that's almost how you do it, what your policy is. And you don't want to impose policies early in the game, okay? Because they may be different policy.

1:05:49
So different groups in the company, they go into different directions and come up with different ideas and then find among themselves, which one should be actually inland. So I started this motion and the very first thing had to do is a fact that the cabin nearly should be moving, one floor.

1:06:09
So coming.

1:06:21
If it's game and pains more of the men and the copy direction is up.

1:06:40
In the next day, he should have done that next floor.

1:06:54
So basically, this says, two things, if you are telling me that your direction is up and you are on the fifth floor, the only thing you can do is go to the sixth floor. You can't go down and you can't go to the seventh one. The only thing can do is go to the next floor.

1:07:14
The problem with this is the fact that what it happens. If you the alarm goes on the Amazon, we know that when the money is only has it should be going down. So I need to account for that. So, I would have to say for

1:07:39
Reaction. Not. So that two things that can happen. One is that if the cabin election stays up, so this is false. Then I need to go to the next floor, but it's possible that become true. And then I don't have an obligation to move, you can do the same thing for the forgiveness going down.

1:08:16
Some games to be more than one because, you know,

1:08:53
So if you see it, you trying to constrain all the movement become disappointed that I request. It's already got us all this fire punching a blessing. This his rules are saying that you need to be able to mean if you are moving. We have to move only one foot That's all they say, so it's very narrow and that's that's what we'd like to separate a specification because very easy to judge about to understand why they stood to go on forever one product.

1:09:32
Now.

1:09:38
Doesn't if there is no direction that you shouldn't be moving. So we have another simulated coming location, okay? Having the election people done.

1:10:06
What you want to say? You have to say that state except for me, the direction changes. Right? So, what we're going to do about is an, unless

1:10:31
So in order, this is not an obligation is not telling the elevator that it has to get out of these. It just says that you cannot move under such time that, you know, the the direction is no longer.

1:11:04
No, depending on what you want to can have different different rules. So one of the rule that I chose was it if you have stopped at the floor you have to stop at the door. If I wanted to say that it's not even guided says, can't be location, okay?

1:11:30
Cabin direction. Equal man. Implies more.

1:11:48
So you may have different policy. If there's no direction they need the doors are closed. You can have whatever policy. It's just an example of policy that you could. All right? So this goes with motion. The next category is my point immediate.

1:12:12
Service.

1:12:22
More people know, we are trying to replace all this. Formul with whatever writing on this board. No, so we don't have enough to be able to prove any of this. So immediate service obligation. That's two things. One is bills with the fact that you are actually servicing very fast but the other thing is that if it says it is not acceptable for later, we have a request on this floor and not service.

1:12:56
That's what really sets and Hello In a multiple elevators that is possible that you're going to do that. You might be there. You say elaborate one is going to pick up this and that about a two weeks of that. So then so that enters specification because very difficult but one elevator, he got going up and I'm pushing the button to the lock.

1:13:24
He better stop, that's not the second. And So the formula will look something nice. And this is the interesting because you with the right form as a related to states and before and after type thing. And so we wanted the post state to stop at the door, reset the button in one of that but we need a pristine.

1:13:56
So some of you uses a pre-state, I arrive at this floor and then I applied to all of the doors. I saw again that would require to stare to phases a rival and then processes since we have not introduced that concept, I need to be able to do it in one step.

1:14:15
So the only way I can do it is by basically saying what I'm in this floor and heading up and that the requests are there, I need to stop there. So it's between I made a decision at the front seven to stop employee which is not that reasonable for elevators.

1:14:36
They need to plan their motion if they're going to fly and move over five floors. Then they basically what they do. They know, the speed moves acceleration, that these operations anything, the only one one floor, they do like, you know, like this. And they do many, many floors. And people like that different different speaks they have there is that animals scheduled motion schedules.

1:15:05
So this is reasonable to approaches, so let's see. I've been on location.

1:15:14
And cabin direction and there's an optical if Kate lost one. So the next floor there is an or there's Italian question.

1:15:39
On K-Pass. So I sent both what there is a cabin or floor, because as an matter,

1:15:54
Your operation here. The next day is going to be.

1:16:05
K plus 1 about and not in plus 1 and

1:16:19
Pretty quest and plus one.

1:16:29
Okay, all right. So as true to this education, missing cases, what you do a relationship be Convene business.

1:16:58
I think it should be. Another originally thought was about.

1:17:08
Basically, this relationship between these two and here we have the requirement to move from the mental move to an explore. And this basically says, if you are in this state and for, okay, on where I would for kicking plus one, the thing that they feel is fire

1:17:40
If the father on his own obligation for service is request. So remember everything with me was we served as a request one way or another, back to starting a certainty. Or by treating the firearms can be served basic cancer and you can then, and so that's and then be the same.

1:18:17
Is there requests if the candidate is down? And that requests down the airplane.

1:18:33
Okay, No.

1:18:43
We still don't think enough. Yes, here we go. Right underneath another deal. What that? Why? What do you choose and deal? Because there, you know, there's no obligation to move to Mexico and you already satisfied here. So in order to go down that you have to move. So here we can basically say what when you're rather than for our wife's mistakes.

1:19:16
I don't I'm I don't have to be the same people, I don't see them, having an idea here or do any damage finding that very good care of that population. So that obligation what is you have to change the state in these matter to do the service and the asset are the more thinking kind of here.

1:19:43
So, we don't

1:19:48
Okay. Now, even what we have is still not enough to prove our properties. We don't have any rules for changing direction and we don't have in this. This property is anything that is forced into there to go down to the first floor. So from all this property that we have here, we cannot recruit this.

1:20:20
There's nothing, he ended with so clear. You have these things more missing more stuff. So we did without us how this element in moves probably separate everything else. We dealt with service requirements, immediate service requirements are. And now we need to deal with the managing direction. If we manage direction then we know how it moves.

1:20:51
It moves under the foot that the rules of the heat. So money is connecting the same. Exactly what we did was it was a break for the car. You control the brake, everything else, you don't care, your consequence of people controlling the brake, you look to the state and based on your state.

1:21:06
You decide. How about the break should do, it's the same thing. We look at the state envision, the state pretty decide whether the direction, what happens with that direction? Well, the cabin moves according to this rules and service is according to this one. So only please control the direction.

1:21:25
But after worry about all these other. So,

1:21:33
I've been the action to put up hundreds.

1:21:50
We're okay. Okay. Later, having

1:22:03
That.

1:22:15
Having the election.

1:22:23
So when this is trying to say is that if the direction is up, he has to stay up.

1:22:34
Under such time that we, we have no requests to buy user. So there is no reason to talk about And the calculation no longer not. So this is basically telling us when we switch from some of you to the policy of very simple policy. It says, you go all the way up to the end.

1:23:05
Want to reach and turn it down all the way down to one and want to reach one. You turn it up and then you don't need none because you just going back up and down there and down, but it's more energy efficient. So if that not request, you should be going.

1:23:21
Yes, there is not exactly by alarm but then that's a very good question. But notice what this sets, they are no requests about, you know, what happens with alarm goes off all the requests and cancel. Yes. So, this becomes, So this is satisfied and he satisfies, this will become of the last election away from us.

1:23:58
Now, we have two choices that we got because no longer are can be as a down on or not. But we don't care, which we don't want to put in this rule. What the con which one which is basically to say we we no longer go out, that's what the root says.

1:24:16
So, this is a rule of when you stop going, that's what the rules, then. You do the same thing for going down.

1:24:28
Leg, don't worry on this.

1:24:38
My only K.

1:24:43
Is more than type of location, not request.

1:25:03
So this is the room. We no longer go down when normal we're done is nothing below the children requested and there's nothing again this could say I mean we're allowed to go up or do have not direct. It doesn't constraint then and guardian.

1:26:15
So notice what's happening here? This is saying that if there's any requests anywhere, you cannot have no direction. You need to learn obliged to believe that.

1:26:37
So that takes care of when we switch directions. Basically, we switch direction. When there's nothing to start with above. Or there's nothing to service below. And you have to options in this and allow us to respect the presence. Either going to opposite direction, but don't go on opportunities. There's nothing to be serviced there because of the rule, so going to answer options, which they could not.

1:27:05
Okay, this is fine that allows us to do the process. So this basic allows us to go up according to this rules. And when there is no more need to go up, we turn down or we stay with nonetheless. There is nonetheless not only requests, but if then in the request we fully option is to.

1:27:30
It still doesn't give us a fire.

1:27:36
So you need to add the rules for the fire by the guardian.

1:27:46
Having location scared of the one.

1:27:55
On implies having patient current direction.

1:28:13
And then I've been knowing about him. He says, I've been location people's one and

1:28:26
On implies.

1:28:42
So now we can look and say, is it possible for the model to have to prove those properties that we are supposedly refining. So what we need to do next would have to they each only this properties in order and and show how you can derive this property from this department.

1:29:08
So let's stay for instance, find a lot of results on until Florida. Alternate one is not.

1:29:22
So how would we kind of wave our way would have to be formative by our way. So we know that kind of the problem is all According to this situation. Here we have two options where these are the four above or whereas the 40 on the floor. You find the first floor, where we're done, combination time.

1:29:49
And,

1:30:08
Happy. She's none. The promoter is over. So we we know that these implies are full noticeable and that's what we wanted to happen. Here over is, overcoming the issues. So we have to this until because of the limitation, so for the case. So breaking into two cases case. One we had in the first floor you have the first part.

1:30:44
We think file our own 10 + 4 implies this. And implication is also not necessarily. Okay, so together for now, if we are in our upper floor basically that says the cabin reaction, it's dumb. So we need to be able to get to the first floor, so now we have to go sooner.

1:31:14
So induction process. So we select the metric. The how many floors instead have to go down to one? And then we use this obligation here to show the metric goes down by, How do we know that the television balance is because we are assuming the thyroid zone, which implies based on that rule that the conversation is done.

1:31:46
So then this part is satisfied. That means that we're going to reduce a metric by going to the next level. And this is false because the fire is going on. So this is false. So we go one level below. So. So the induction that eventually get to first floor and we have already troop on the first floor.

1:32:11
So basically we in separate two cases. One is basically an implication. There's a part is an induction, at least two and induction on the distance from the floor. One for five, the metric is four for one activity to zero and with and that's a way to have the food and you have to do this for all these problems.

1:32:43
Now what I explain to you them to prove, it's a reasonable, I mean he's technically a solid but there's no guarantee that may not be problems. So unless you do it mathematically what it really is using almost always have some possibility and that's what makes this you know disapp.

1:33:17
From the treatments for the treatment, but you know, verification is easily created. The other thing is that there's something called validation. If this weather customer wanted we are the will overcome a judge and execution that. Right? So we basically, we are the customer so we choose what everybody was nice and simple for us to do, but the customer they know they want something different.

1:33:45
So just the process of doing this first thing has to take part of the week of time in particular, what the three iterations would even involve doing a simulation actually computer. Simulation the elevator and check that this rules, apply to the to the simulation and make sure that the customer of these.

1:34:09
So, delivering code. That is perfect writing requirements. That are but list thinking about formally it allows to clean out some of the English thinking and also one of the things that I hate is, I'm, you know, I don't in some of your previous sections here is just became very messy.

1:34:42
I mean, there are too many people to go and try to fix a little detail and just kind of put it out a few things actually obvious, but you know, just look at took complicated. So on specifically, you're complicated the basically start telling you that you need to rethink how you organize.

1:35:01
I mean, I didn't know if I'm off with this, you know, just, you know, three minutes and think about it how to separate the different. The different kind of requirements. What is good terminology to use? So, I separated the motion from the control of the direction. So, basically the movement direction, but from the motion itself, the most amazing users, it's kind of like the modular.

1:35:31
The computer that says, you know, what am I jokes supposed to be about? When I look at this very little okay but that's a controller to that part of the policy and the policy can get maximum complications. All right, let's make a break in.

1:36:15
The very first time this war similar, he's just saying so very much the sound variation. Oh, so whatever. You also three years now? Yeah, I'm just saying that the requirements for the down version or basically, the same as the F1 was mere you.

1:37:04
I would say as well. I have had like an absolutely job shopping for and then I promptly bought the once a year ago before most importance like said, wow, she gave us the easy points out there, not in blood. Those multi answer ones was I put like three of them from her age about and I took away the rock, the right answer and left

1:37:47
Rules.

1:39:39
Hey.

1:40:11
For false questions. But,

1:40:19
The times, but something. Yeah, I think lot of my success came from being like, let me think about her personality. No, I was like more more negative answers and positive but it's true a lot more false than truth and so those questions were different but the long answer questions were pretty hard.

1:41:13
But,

1:41:18
Like who was like, hey read this description before that sounds and then I remember talking to you and it was like you

1:41:44
So, pretty standing on, yeah, for now and just my thought was, I don't want to get second school, but yeah, I wear mask in.

1:42:02
Yeah, not required to show telling more masculine. I mean I hate teaching and I'm trying. You have a lot of I don't mind with people who are presenting take their assets offline. I don't really think care about it a whole lot either way. It's just my preference. So I wear it.

1:42:25
I it's just really ugly facial hair right now so I think I'm just really not thinking, so that's my official hair looks good. We always reading deeper into the statement, you know, make sure that at the end of this semester

1:42:54
Is another in Texas? No, they are in the Connecticut nowhere. But yeah, I thought he said, Austin former student friend of mine. She is. Okay, so we will around zoom every week that you can have those things.

1:43:29
Project on cyber security event, interplay storms.

1:43:39
And I want to use class applying to that to be able to take our to be different. I mean, if I'm successful in the very first formerly, very far middleware.

1:44:01
Can't be and I need and that would have been the cat's meow. And both of the same. Okay, I've never heard cats looking.

1:44:22
Coming. That would be high vector.

1:44:28
That was, I had somebody with ideas but

1:44:35
Because this person, I mean because scientific names how do kind of specifying, security requirements, verify security require and how do you design the system to be secure onto very high? The system requ to do a huge. Am, there is a again external that has been funny and years really huge.

1:45:08
It's until that, the only is only sec.

1:45:23
Forth. You say you have a postdoc who did a router for most personal salt? Did you do a publication for that? So, put the name of the publication Google. You it's probably still references from all one more rock is going to human routers. Your next assignment is going to be around.

1:45:55
Oh, and I think that, you know, he did a former refinement of the process. There's some very sophisticated six months from that work, all right. In the transcending of the doctor degree that doesn't seem like a disposal. You already had a doctor so it doesn't that they would like and not a long time either because probably honestly when you're posting may have felt like forever.

1:46:26
Just still be. Okay.

1:46:33
So, who's going for a doctor here? Maybe I learned. Are you seeing it? Yeah, I don't want you thinking about doctor, all right, you know, you're right in the program. So, okay, so so you raise your hand. You want to be Well, I should get to get you all to raise your hand by next week.

1:47:05
I mean, it's a five-year commitment after including the Masters but it opens up doors and gives you freedom that can come in and anything. It reached some my college, basically, this government money for 10 years to develop some multicast routers. And then they started based on that very technology, that was funded in millions of dollars for 10 years for the government.

1:47:36
They opened up a company and Cisco. Both them out for 36 mayday.

1:47:50
So that's another, you know, that's another way how you can get reached by being, you know, the first brand programmer that Microsoft in on the first content employees, that's another way to eng but they are not coming here, it's easy. But if you get lucky but I mean, if you want to, to be big person involved in the technology and

1:48:17
You need to go to academia so you can have the freedom to to do your own research and then to start the company from. I was not very entrepreneurial. So I had either, we had a couple of presentations that really could commercial about, you're not the strength or net interest.

1:48:38
I said I wasn't going to do it by myself. So then you have this of a reference for this course because I think, but I didn't say I mean, you have this for mobile computing but I think there is no such this in this course only syllabus and and because I'm really yeah because I'm relying on doing right here.

1:49:15
There won't be there because you left to go to my website to my resume. Oh, okay. Or just go we have because we have been doing everything base kind of focusing on the they're not additional readings. Oh except for this logic. Oh, okay. So, what we're gonna do today is the time it's left.

1:49:40
No problem wasn't was very important, that was really helped. I mean just I mean I didn't pay so I but so kind of relative to the night before based on. I had all your assignments open, and I was looking at how you're thinking in the most ideas were there, maybe I missed those.

1:50:16
So I analyzed all of that to rewrite. My my sol I have enjoyed it. So what we're going to do today is we're going to do a case study on the shortest path.

1:50:41
Now, compliments things to think about them. First of all, children's past is an important problem. If you are not thinking about it, these women, your computer is thinking about because your computer is getting targets. So the internet and you know how this bag has come on the short response.

1:51:07
So there are huge investments in thinking about algorithm for the shortest path. You're not going to be not going to study them for their purpose but I mean in this class the kind of case studies and problems so are selected to be intellectually and practically import. So the short path is an important problem.

1:51:31
That what we're going to do today, we're going to start thinking about its process of refinance. The holy grail of former methods people is that you start with a sophistication, which is five lines. Then we find it to 20, then you're refining to 100 and you're not a southern then you got just 10,000.

1:51:55
And then when I got to 10,000, they give it a compiler. I turn into the code and say goodbye and you go to home because it's currently to be correct, because you've done all this proofs you and you use me, you know, when you move from gun lies to a hundred, you know, there's a computer there, the checks that you're reasoning is all correct.

1:52:15
Now, I like I said, I'm not into make, that's a huge amount of research in this country. Proves I'm not the best for me that I have been exposed a little bit with another expert. I don't really enjoy doing that. It's, it's a different kind of work. I like to think more.

1:52:34
I mean oranges in concepts and but even that, you know, that that way is thinking what you're going to try to look at today's basically look at how people approach a problem and develop the problem from the start, the specification and drive the other way You are doing something that but you're not really.

1:52:58
A kind of, you know, the kind of assignments. Someone like this specification and sometimes you get provided by the spec but you're doing in an automatic. So basically you look at this, the spec or the requirement or whatever, the homework does and then you come up with a solution that is, there's a kind of miracle in between You've seen those cartoons but you know, a miracle happens here.

1:53:23
So you go from one to this because you already have smarts and you can think but you're not really going step by step and it's not easy to do it and requires somebody going to skills. So this is really an example of how people might approach things, right? Formally in most steps by step.

1:53:46
Now, I also have acknowledge that we're going to develop, you know, design different algorithms for same problems, like code for the same problem that code already existed in the. But the authors started as a bank and what their way through and showed, how you could have uncovered those solutions.

1:54:12
This is come actively, but still yeah, it's very interesting. So, let's throw the sign that you find the problem.

1:54:29
And then we might get right. I think it's sloppy sometimes don't be ashamed to me. The way we push me down. Put me down country. So, we have G, which is a graph.

1:54:57
Ver, kind of and the edges have a direction which is direct, so verbism would be from zero.

1:55:16
In for higher.

1:55:26
We're also going to so fast ij basically that the past from I to J along the British. Now along the vertices of the edges falling. The correct going to engage. So it's basically a sequence of address.

1:55:55
You can hit the notion of a cycle.

1:56:01
Into pass pain. Sorry, so it's a closed loop. No problem with the address and you get back to what is different. Now this can be forwarded defined, I'm not going to puzzle from the time. Because we understand with what they need in front of the area cannot also hit something called weights.

1:56:46
So, this is a fab in. There's another same man I win and communicate same thing. Whether it was, but these are basically weights values that are floating point number. So basically what this W does it takes every for every edge, it gives the weight, how much that can manage dentists is going to work?

1:57:15
So you can think of it as in networking the weight has to be but can also have to use a cost. So the reason we want to show this path, we want to start this path, not just in the number of parts, but number some of the ways. So, we've paid the least amount of money, you know, throughout our packets.

1:57:39
So that to that part that.

1:57:45
So, the best length is in some ways.

1:57:59
So we need to talk about the shortest path. In one attached to shortest surface lengths. Which means in some of the ways has to be resp.

1:58:13
That's that's what we say. You have a past with the total weight of 15 and the weight of five. We want the one response.

1:58:28
Now, so this is kind of the nature of the problem we want. We want to find out this shortest path between a repair of those IA. So these are nothing, you know, to send the packets preferentially in the shortest way. Now, the shortest path, sometimes is other interpretation which is a short number of parts.

1:58:53
It's just not. So we can have a pass which as many hearts. But the post is lows that subsided on the one up, but the cost is hard. Think I'll pick up your, you can basically route your packets, to many, you know, intermediary nodes that are all coming public service nodes.

1:59:14
That of course, do nothing versus using commercial pipe, which is very expensive because can provide a high quality Now it is useful. When you talk about this problem, we introduce something called over a way, 80 weight matrix.

1:59:44
Which was it does, he takes? And then, so corresponding to vertices and maps it to wait, So it may look like this is the same thing, but it's not quite the same thing. The this weights are laughing from edges, that exist.

2:00:19
Some values. It's a mapping for edges, which may or may not exist. The valence. So now we are signing value to every every pair of vertices whether those were disactually exist in the graph or not. And the way we do that, basically the small

2:00:50
By J is definitely small IJ.

2:00:58
And you know, so if the hedge actually exists, we give it the correct weight. That is in the ground will be happy to infinity if it doesn't exist.

2:01:19
And exactly 0 is

2:01:27
So basically, we create this loops and don't exist in the crowd can begin, went to z

2:01:40
If we have this definitions, then we can introduce D which is a shortest lines.

2:02:10
So this is what the result that we actually want to compute.

2:02:22
So we can look at the graph. We look at one possible path. We paint just to nodes. And using this edge width matrix, we compute the sound and for that, we get to get the shortness. So, we can get the shortest past, given between two nodes and connect it in the way.

2:02:47
This was the infinite equivalent. So, even all this definition working, we need to produce. Well, this program, which basically says through, it's to fix point. Basically, the way you read that in English, is that write the program switch in a final number of steps terminates. Let's fix one. Is termination is for us.

2:03:23
Okay. And then what we want, we want determin. One of the could give us a desired result. The desire is all these, this this maintains, that's what you want to get. But this is a mathematical and concept, so we need to have a valuable then points again. So, you have to pay a little D in that same time, specific.

2:04:03
So blower springs. Point be, which is a matrix contains all this the shortest path or and okay. Okay, let's take a picture here.

2:04:28
You see better here on. This doesn't mean it doesn't matter and I don't think it matters. Okay. So, is not zero.

2:04:50
And,

2:05:05
And they just have weights since

2:05:15
Say.

2:05:20
Okay, so if we just look at

2:05:31
The names of them in the shortest lens. The shortest path between zero and z. Well, how can I get from the other facility? Well, so for told his man, yeah, it's better.

2:05:58
So we have started zero and we can go on this path to six. So this path zero one, three gives us the the lens we had to go this way zero. One, two, three plus two. Plus one plus two gives us five which is a better way to pass.

2:06:25
Or you can go this way. Three plus two to the shortest. Sure. This past is fine. You care. What you have to be taking. No one's longer doesn't matter that we want the value of the shortest path. That's okay. Starting in the, in a little basis. See because this person is from zero three.

2:06:55
Give me a value and that value must be the shortest. They cannot be a short that's more about you on any event presence. Yeah. Would you want to choose? If you which part you don't choose a path of when you choose a value of your? So we are interested in the smallest value.

2:07:18
So, we consider all paths. We had three tasks that we can go through and told them that it happened to everything. Value doesn't even matter which is chosen small as well. Now, if we talk about the, you know, the past from 3 to 0, we see that this past here, choose 2.

2:07:42
And that's only way to get some. So if you only have a little value, if we have another note here for and there is no collection of the graph, then from 0 to 4. The value will be because now don't be some cavities again. Okay, so we just basically have to like program the program, the computes, you know, all this distance.

2:08:13
So with very simple one, basically you could write a code that turnates all the paths and whatever, guys. You generate all the values and then you find a minimum and that's what I'm asking. Okay. But we want to develop these kind of in the kind of systematic, systematic way.

2:08:38
So, we have necessification.

2:08:46
And I want to point out that, in this case, you see, this specification is still as long, but it still has long because, without two pages of text in front of it, includes both definitions and explanations, and so on. And that's why.

2:09:07
Okay, so we want. So what we want to do, we want to do problems because what is it? We want to start with respect. This is given to usable and we want to refine Jane. Got us specification, which is more here. It was programming, then when you define the specification, then the right code, that matches a new specification.

2:09:35
That is kind of. So the specific news, specification should give us a hint of how we might write the code. That's a whole idea that looking at combined looking and respect. You can come up as ideas on how to write the code, then you define the specification again. And there are other code sometimes, as you develop the code, you give you some ideas of how to refile the specific.

2:10:03
So, so they refinement doesn't come immediately from the spread. It comes sometimes from the people that do this, you know, they they just have a set of tricks. Like for instance, you can see later on. You can have a, if you have a centralized value and you have a distributed computer, You know, that centralized value, you have to choices either into the center as well in one.

2:10:32
Simple memory. Well, you have to distribute the value. So there's something called a weakened in process. So each one of us might have an approximation of that value, but as we move, you know, we all synchronize and and converging, same set of results so that different strategies. So the first we find them is one in which basically what we're going to do, we're going to, you find them the fixed point and then introducing an guardian that kind of shapes the, the way we do things, the way, we're a lot of the things and then we also going to develop a metry because you're going to have to show that from true.

2:11:31
We get into the fixed point, so we're defining this and then refining them finding this by conditioning metric and finding that by basically writing down the what the fixed point might be. So, here's and find.

2:11:56
So we have fixed point. He gone portable. IJ to be IJ. You know, a big allocation is a variable that her homes are should in the end. Hold the result so DIG equals. In the okay. Be like, okay he

2:12:38
So so what is what does you saying? It's saying that basically BIJ halls actually the result of we want you know that we want to have in the end. Because see, this is supposed to be the distance from I to say hello. The minimum distance, right? The differential motor path.

2:13:00
So what we've done here is basically we consider all the tasks that goes through, okay? They want to see four five, six, seven, and we sounded too bad because if you're from, I to J in this game between, we have to sum this branch and some days, so it sounded too bad.

2:13:24
And we take the minimum because of all these possible death so that's it's ready to do it. We're taking where basically describing all the paths and there's not none of them know that excluding and then we take the minimum value. And that's what we we had to explain the action, The other property putting onion.

2:13:59
Has two parts. BIJ is more than equal to WIC, and let's just look at this part. WIK was this.

2:14:17
So this is the original knowledge that So the net matrix, you know, some some things have defined is way some value. Some things are infinite. Resources are zero. So we need to do better than this. We cannot do any works. So that's what the first part of being guided, The other part basically says that the DIJ and in English Case of the length of some

2:15:11
So we're not. So basically this part is saying you can't introduce past that don't exist. So I need to use pass and to exist, and then and you have to make sure that God actually improving overdose law. And the third part. It's a progress. Basically says if you are not at this point and they are mentioned and you're going to see that, this is a matter that has it's kind of a has two parts and often metrics.

2:15:49
Have we tended to have metric with one value but we can have metrics that can be fact. So, for instance, this is called run become a sum.

2:16:07
People. And each two another smaller than

2:16:26
So what is not?

2:16:39
Look into this matrix here.

2:16:45
So I can have a path that goes through a missing edge once await on the missing edge. Infinity. Okay. So, I can now refine things, but infinity minus 25, plus 36. So infinity, it's sunning up. Infinite is, it's makes it difficult to to measure problems. The way major problem.

2:17:22
One way to measure progress is that you've got to pass which is not even, so, it's not broken fast. Okay. And gets a better value. Another way is to discover an edge helps removes any? Because now we have a past and that before. So what mom is is a number Infinities and some he's really the summation of weights.

2:18:00
That I'm not infinity.

2:18:10
You should because you just combined it too.

2:18:26
Just to make sure that

2:18:36
So, none is sort of some I'm Jane. DIP something is infinity one, so we can't get for every DIJ were the best distance of our is infinity because it's one in and for others.

2:19:22
The way we make progress is by basically reducing the value for B. So if we settle these and they just some paths then we'll make getting closer and closer to the, to the goal. So that's what the sound part is now has to, you know, keep track of the number of humans that used to have.

2:19:46
So we can make progress by replacing an impedance after value or something is my state there. If the CSR teacher, you have everything.

2:20:07
So, So that's a condition in the metric and what is saying it is smaller than you compare the first term. The first term is smaller than it's smaller. It is first term is equal, then you compare the second term and then so it's exactly like a pyramid place. You don't got to go orders, sleep on one versus four point two or three.

2:20:35
It's larger than say by one. Okay, so now what we need to argue is that

2:20:50
You need to argue that this refinement actually is to correct requirement of the of the two. So we need to basically first of all can show that if we take these two pieces here that's there, I'm going to give us a desire itself and the way this is done is buying.

2:21:30
So basically, we want to show that if we take property, one can be played in the two. That implies the, that's something because this is what? Our Thanks buddy. Supposed to be equally Lord is equ covering, right? So to do that, we actually want to do it by induction.

2:21:58
That's a part. We need to do is even if metrics show the fixed point. This is rich. So the magic thing, we this basically says that the metric decreases. So it's not like you have the program and you look at the program and basically the problem if you already said the our program to have a written satisfied property, we decrease the metric since our product is the metric.

2:22:31
And this is well, founded is it's always red is on a nickel. Then zero carbo zero. Okay. Then you can, you can conclude that. Actually, at some point we can all over decrease the metric and therefore the fixed point is now In the same country, I mean the same kind of reason.

2:22:52
Yes. Which is basically helped to show the metric metric increases It decreases whatever. Then it means that the average means that this piece is true. So that's the way to do that part. This property here to do this other property here. You need to show that this two and not implying that, you know, we got them, the correct result.

2:23:21
So the way that is by induction. So, we do an induction. And the length of the shortest.

2:23:44
You can, you know, can be very can be very complex and they many different forms. So the base case, we assume that the lens is 1. So our business, okay? The strongest pass is problems one. Well, if the shortest person on less one, then the DIA is equal to W.

2:24:16
J. Because there's only one edge and that's our regional and that's a, it's a business or that one edge. So we do have the amino distance the carbonyl, there's only one edge that exists so that has to be the only since it only one is a meaning down in the darker step.

2:24:53
Basically is we consider them the past.

2:25:02
From x to y is of.

2:25:09
And last one,

2:25:15
I mean that's the way that I'm doing actually so that the base case is still in the m is true and improved for impossible. So if that's a case and notice what we're doing, they've already been many coded. We are actually beginning with the specifications openly. Write the code before the hours.

2:25:37
Okay? So in the past it's like this. Then the passes should be kind of harder to be big prime and see one.

2:26:02
Where the prime is or less than and this is one more. So P is not of an example as one. Now we know that this is a shortest path. Okay. So VXY, he's one of them. He has these more than plus the z1.

2:26:34
That's,

2:26:40
Now, this is also the real path because you made it sound for them. This is a fast in between pegs and why? So, here fast.

2:27:04
So since we know that this is a disease, I mean, this is smaller than the sum of them. And there we know that the shortest that this is the shortest path and we are just adding one more element then deal. XY should be going to the next one. Can have a this this part that's already improved and this is a short complaining better than and we are extending it.

2:27:48
And this is the, this

2:27:56
Shortest path of legs. And plus one. They cannot be a shorter path because of the assumption we made. So then it has to be to be and you don't need to consider any ads longer than m plus 1 because we assume that the the paths between x and x and y is over plus 1 levels.

2:28:26
So so that, so they can't be any initial of that. Well, once once you do all of this work, then accomplishes that you you may want to write film.

2:28:51
To the strategy of learning can use is that, you know, how you get the fixed point from the program, you based colony, form, physical and in a judge office at the code from the fixed point. Are you picking the equal who's calling? So, the program.

2:29:35
To resp was and then the science.

2:29:55
And again, we can kind of

2:30:26
Okay, so let's change good is at the meeting over forward. So we have on our path there. We have a zero to one.

2:30:44
So it's so let's say that i is 0 and let's say genuinely, have to give you direction, those are all the points. So basically he says hey the distance from from i to zero which is zero to zero at zero right? Plus the distance from zero to three zeroes to see doesn't have a very connection, right?

2:31:17
So, the infinity

2:31:25
Take one. So we have from 0 to 1. 0.1 is what the two.

2:31:38
Then 0 to 1 and 1 to 3 1 to 3. We got a 6. Just anything from zero to two 0. To 2 and 3 can two three. I'm gonna do. Okay? Because it's a five and then from zero to three we get infinity, right? And from sleep is being against zero into the name, from all of us.

2:32:33
So you you have an end cube number of processors. We can compute this summation in constant time. And then Yeah, then you have to compute the need. Many usually lower because it's like a treat and organizing the tree. So there you have a login and then you need to think of how many steps it takes and you can prove it actually.

2:33:06
Thanks all. So, so what happens now is that we started this specification when you find the specification, we show this was vacation. It's a great refinement. Then we know the code inspired by specification and you can prove it a code means a specific to prove. That because only beauty phase is by equal and we can.

2:33:32
Okay. And so, and then we have to ask us about targeting. Thank you. Example, was if I have an end to the third processors, you know, I can, I can compute the summation and kind of one one step then I have to do the immunization. So, it's not because those you make a tree like this, that, you know, again, and then you have to reach things from.

2:34:13
And you can feel this also many. So now I need time squared gives you the perfect algorithm and again, it's important is driven home is that the capital of complexity of any of our alcoholisms. Unless you think about architecture that's connected? Thank you. So with this program, only worked for a blanket too.

2:34:45
No. But you see we had already four girls. So before we had before nose, you can only have most of her hair between them even more knowledge. So they have capacities three to the levels if you have more than that change. Well, so you need to know what they did this because

2:35:19
So, if you weren't back in the okay, more time for

2:35:43
But once you continue to lose it next long, they couldn't and really looking at this nodes path. And not. The next.

2:36:22
We have.

2:36:46
Yeah. In the, you know, it's allowing me to dec because if they need something doesn't mean that. So, the equations. So either way just a separate Here in the assignment makes a video. But here it doesn't behave to make it simple for people to be able to use