1 00:00:03,860 --> 00:00:09,380 In this video we're going to begin our discussion of formal operational semantics 2 00:00:12,820 --> 00:00:17,621 Just as we did with lexical analysis, parsing and type-checking. The first step 3 00:00:17,621 --> 00:00:22,361 in defining what we mean by a formal operational semantics is introduced the 4 00:00:22,361 --> 00:00:26,978 notation and it turns out that the notation we want to use for operational 5 00:00:26,978 --> 00:00:31,965 semantics is the same or very similar in the notation we use in type-checking. We 6 00:00:31,965 --> 00:00:36,927 are going to be using logical rule of inference. So, in the case of 7 00:00:36,927 --> 00:00:42,175 type-checking, the kinds of inference rules we, we presented, proofing's of the 8 00:00:42,175 --> 00:00:47,902 forms that in some context. We could show that some expression had a particular type 9 00:00:47,902 --> 00:00:53,059 in this case to type c. And for evaluation we're going to be doing something quite 10 00:00:53,059 --> 00:00:57,379 similar. We will show that in some contacts now that this is going to be a 11 00:00:57,379 --> 00:01:01,699 different kind of context that we had in typing so this is going to be an 12 00:01:01,699 --> 00:01:06,506 evaluation context as oppose to a type context and so what goes in the context 13 00:01:06,506 --> 00:01:11,495 will actually be different. But for the moment all that really matters is there is 14 00:01:11,495 --> 00:01:16,302 some kind of a context and in that context we're going to be able to show some 15 00:01:16,302 --> 00:01:23,044 expression evaluates to a particular value b. So as an example, let's take a look at 16 00:01:23,258 --> 00:01:28,667 this simple expression, e1 + e2 and let's say that using our rules which we, I 17 00:01:28,667 --> 00:01:34,432 haven't shown you yet, but let's say we had a bunch of rules and we could show in 18 00:01:34,432 --> 00:01:40,523 the initial context. That e1 in that same context, okay? So these context are going 19 00:01:40,523 --> 00:01:45,908 to be the same, that e1 evaluated to the a value of five and e2 also in that same 20 00:01:45,908 --> 00:01:50,894 context evaluated to the value of, of seven then we could prove that e1 + e2 21 00:01:50,894 --> 00:01:56,279 evaluated to the value of twelve. If you think about it what this rule was saying 22 00:01:56,279 --> 00:02:01,597 is that if e1 evaluates to five and e2 evaluates to seven, then if you evaluated 23 00:02:01,597 --> 00:02:06,550 the expression e1 + e2, you're going to get the value twelve. And what's the 24 00:02:06,550 --> 00:02:12,313 context doing, well it doesn't do a whole lot in this particular rule. But remember 25 00:02:12,313 --> 00:02:17,701 what the context was for in type checking. The context was for giving values to the 26 00:02:17,701 --> 00:02:23,153 free variables of the expression. And so, we need for an expres sion like e1 + e2 to 27 00:02:23,153 --> 00:02:28,411 say something about what the values are, the variable that might appear in e1 and 28 00:02:28,411 --> 00:02:33,668 in e2 in order to say what they evaluate to and, and therefore, to say what the 29 00:02:33,668 --> 00:02:40,301 entire expression e1 + e2 will evaluated to. Now, let's be a little more precise 30 00:02:40,301 --> 00:02:46,843 about what's going to go in the context. So, let's consider the evaluation of a, a 31 00:02:46,843 --> 00:02:52,976 expression or statement like y gets x+1. Okay, so we are going to assign y the 32 00:02:52,976 --> 00:02:59,763 value x+1 and there are two things that we have to know in order to evaluate this 33 00:02:59,763 --> 00:03:06,052 expression. First of all, we have to know where In memory of valuable start. So, for 34 00:03:06,052 --> 00:03:11,270 example, the variable x here, we're going to have to go and look up excess value and 35 00:03:11,270 --> 00:03:18,236 then add one to it And then that value is going to be stored in whatever memory 36 00:03:18,236 --> 00:03:25,625 location holds the value for y okay so there is a mapping from variables, Two 37 00:03:25,625 --> 00:03:34,602 memory locations. Okay and that is called, In operational semantics the environment 38 00:03:34,602 --> 00:03:39,152 and this is a little confusing maybe because it use environment for other 39 00:03:39,152 --> 00:03:44,139 things. Okay, so now let's forget about, as all we uses of the word environment. We 40 00:03:44,139 --> 00:03:49,001 were talking about the operational semantics, what the environment means is 41 00:03:49,001 --> 00:03:54,112 the mapping, the association in between variables and where that variable store in 42 00:03:54,112 --> 00:03:58,974 memory. And then in addition, we're going to need a store and that's going to tell 43 00:03:58,974 --> 00:04:04,023 us what is in the memory. So just knowing the location for a variable isn't quite 44 00:04:04,023 --> 00:04:09,488 enough. When we, if we know the value of x if we know the location for x, for example 45 00:04:09,488 --> 00:04:14,210 or as, as important because we're going to get the value of x but we also have to 46 00:04:14,210 --> 00:04:19,951 know exactly when value is stored there and so store. Is going to be a mapping for 47 00:04:19,951 --> 00:04:25,745 memory locations Values. These are the values that are actually stored in the 48 00:04:25,745 --> 00:04:30,419 memory so it's two levels of mapping. We associate with each variable and memory 49 00:04:30,419 --> 00:04:36,708 location And then each memory location will have a value in it. So let's talk 50 00:04:36,708 --> 00:04:41,982 about the notation that we're going to use for writing down the environment and the 51 00:04:41,982 --> 00:04:46,468 store. So as we said, the variable environments have variables to locations 52 00:04:46,468 --> 00:04:51,464 and we're going to w rite that out. In the following way, we're going to just have 53 00:04:51,464 --> 00:04:56,375 this as a list of variables and location pairs separated by columns and this 54 00:04:56,375 --> 00:05:01,351 environment for examples of variable a, is it location l1 And variable b is in 55 00:05:01,351 --> 00:05:06,454 location l2. And another aspect of the environment is that it's going to keep 56 00:05:06,454 --> 00:05:11,429 track of the variables that are in scalps and the only variables that will be 57 00:05:11,429 --> 00:05:16,469 mentioned in the environment are those currently in sculpted in the expression 58 00:05:16,469 --> 00:05:23,126 that is being evaluated. Now as we said, stores map memory location to values and 59 00:05:23,126 --> 00:05:28,558 we'll also write out stores as lists of pairs. So in this case, the memory 60 00:05:28,558 --> 00:05:34,436 location l1 in the store contains the value five and the memory location l2 61 00:05:34,659 --> 00:05:41,029 contains the value seven And we will also separate these pairs by an arrow. And just 62 00:05:41,029 --> 00:05:46,224 to make the stores look a little bit different from the environment so that we 63 00:05:46,224 --> 00:05:51,616 won't confuse the two. There's an operation on stores which is to replace of 64 00:05:51,616 --> 00:05:56,614 value or update of value. So, in this case, we're taking the store s and we're 65 00:05:56,614 --> 00:06:01,941 updating the value at location l1 to b12 And this defines a new store s prime. So, 66 00:06:01,941 --> 00:06:07,531 keep in mind here that the stores are just functions list in our model and so we can 67 00:06:07,531 --> 00:06:12,200 define a new store by taking the old function or the old store has and 68 00:06:12,200 --> 00:06:18,540 modifying it at one point. So this defines a new store as prime such if I apply s 69 00:06:18,540 --> 00:06:25,442 prime to the location l1, I get off the new value twelve and if I apply s prime to 70 00:06:25,442 --> 00:06:32,598 any other location, any location different from l1 I get out the value that the store 71 00:06:32,598 --> 00:06:40,812 held in s, sorry the value of the location in store s. Now in Cool we have more 72 00:06:40,812 --> 00:06:45,585 complicated values and integers. In particular we have objects and all the 73 00:06:45,585 --> 00:06:50,617 objects of course are instances of some class and we're going to need a notation 74 00:06:50,617 --> 00:06:55,196 for representing objects in our operational semantics. So we'll use the 75 00:06:55,196 --> 00:07:00,486 following way of writing down an object. An object will begin with its class name. 76 00:07:00,486 --> 00:07:05,840 In this case the class name x and it would be followed by a list of the attributes. 77 00:07:05,840 --> 00:07:11,874 In this case the class x has n attributes, a1 through an And associated with each 78 00:07:11,874 --> 00:07:17,759 attribute will be the memory location whether an attribute stored so attribute 79 00:07:17,759 --> 00:07:23,496 a1 is stored location l1 up through attribute and which is stored at location 80 00:07:23,496 --> 00:07:29,009 ln. And this would be a complete description of the object because we know 81 00:07:29,009 --> 00:07:34,969 where in memory the object the object is stored. We can use the store to look up 82 00:07:34,969 --> 00:07:42,542 the value of each of those attributes. There are few special classes in Kuhl that 83 00:07:42,542 --> 00:07:47,810 don't have attribute names and we'll have special way overriding them. So integers 84 00:07:48,003 --> 00:07:52,950 only have a value and, and that will be written as int with a single value in 85 00:07:52,950 --> 00:07:58,410 parens, the value of the integer similarly for brilliance. They have a single value 86 00:07:58,410 --> 00:08:03,229 true of false and strings have two properties, the length of the string and 87 00:08:03,229 --> 00:08:08,453 the sting constant. There's also a special value void typed object and we'll use the 88 00:08:08,453 --> 00:08:13,505 term void in our operational semantics to representative and briefly here, so void 89 00:08:13,505 --> 00:08:18,371 is a, a special and that there are no operations that can be before and on void 90 00:08:18,371 --> 00:08:22,868 except for the test is void. So, in particular, you can't dispatch the void 91 00:08:22,868 --> 00:08:28,104 even though it has typed objects that will generate runtime error. The only thing you 92 00:08:28,104 --> 00:08:33,155 can do is to test whether the value is void or not. And concrete implementation 93 00:08:33,155 --> 00:08:39,452 we typically use a null pointer which represent void. Now we're ready to talk 94 00:08:39,452 --> 00:08:44,241 about in more detail what the judgments will look like in our operational 95 00:08:44,241 --> 00:08:49,542 semantics so the context will consist of three pieces. The first piece is a current 96 00:08:49,542 --> 00:08:54,331 self object. The second piece is the environment which is again the mapping 97 00:08:54,331 --> 00:08:59,376 from variables to the locations where those variables are stored and the third 98 00:08:59,376 --> 00:09:03,910 piece is the memory, the store. The mapping from memory locations to the 99 00:09:03,910 --> 00:09:09,106 values held at those locations, All right? So in some context, an expression e will 100 00:09:09,106 --> 00:09:14,509 evaluate to two things. First of all, e will produce a value so for example we saw 101 00:09:14,509 --> 00:09:19,976 before that the expressions seven + five would produce the value twelve, that's one 102 00:09:19,976 --> 00:09:25,250 result to the evaluation. But the second thing is that we'll produce a modified 103 00:09:25,250 --> 00:09:30,203 store. So the expression e maybe a complicated piece of code Maybe a whole 104 00:09:30,203 --> 00:09:35,220 program is on the right and it might have a slight statements that update the 105 00:09:35,220 --> 00:09:40,458 contents of the memory And so, after e is evaluated, there will be a new memory 106 00:09:40,458 --> 00:09:46,226 state that we have to represent and so s prime here represents the state of memory 107 00:09:46,226 --> 00:09:51,985 after evaluation And now, those are couple of things here. First of all the current 108 00:09:51,985 --> 00:09:58,593 self object and the environment don't change. They are not changed by evaluation 109 00:09:58,593 --> 00:10:04,972 so which object is the self parameter to the current method and. Well, the mapping 110 00:10:04,972 --> 00:10:10,370 between variables and memory locations that is not modified by running a, running 111 00:10:10,370 --> 00:10:15,383 an expression and that makes sense, I mean, you can't update the self object in 112 00:10:15,383 --> 00:10:20,588 Kuhl and we don't have access in, in any form to re-locations or variables stored 113 00:10:20,588 --> 00:10:25,472 and so those two things are in variant. They don't they are variant under 114 00:10:25,472 --> 00:10:30,541 evaluation. They don't change when you run a piece of code. However, the story does 115 00:10:30,541 --> 00:10:35,381 change so the contents in the memory may be modified so that's why we need a store 116 00:10:35,381 --> 00:10:40,655 for both before evaluation and after evaluation. And one more detail these 117 00:10:40,655 --> 00:10:47,075 judgments of this form always has a qualification. That judgment only holds if 118 00:10:47,075 --> 00:10:52,490 the evaluation of e terminates. So, if e goes in to infinite loop, then you're not 119 00:10:52,490 --> 00:10:57,566 going to get a value and you're not going to get a new store. So, this kind of the 120 00:10:57,566 --> 00:11:02,914 judgment must always be read as saying that if e terminates, then e produces a 121 00:11:02,914 --> 00:11:12,440 value v and a new store s prime. Summarize the results of evaluation is a value and a 122 00:11:12,440 --> 00:11:18,635 new store. And where the new store models, the side effects of the expression And 123 00:11:18,635 --> 00:11:22,892 once again there are something don't change as a result of evaluation. And this 124 00:11:22,892 --> 00:11:27,258 is actually important for compilation because we'll be able to take advantage of 125 00:11:27,258 --> 00:11:31,299 the fact that they don't change to generate efficient code so the variable 126 00:11:31,299 --> 00:11:35,449 environment doesn't change, the value itself which object we're talking about 127 00:11:35,449 --> 00:11:40,035 doesn't change and notice here as another detail. That the contents of the self 128 00:11:40,035 --> 00:11:44,399 objects, the attributes inside the self object might change, they might get 129 00:11:44,399 --> 00:11:48,821 updated but t he locations where the attributes are stored do not change. So, 130 00:11:48,821 --> 00:11:53,833 the layout of the object where the object stored doesn't change and that's all we're 131 00:11:53,833 --> 00:11:58,491 saying here, the actual contents of the object which of course is a part of the 132 00:11:58,491 --> 00:12:02,979 mapping of the store, those might get updated by evaluation. And also the 133 00:12:02,979 --> 00:12:08,569 operational semantics allows for non-terminating evaluations. That's the 134 00:12:08,569 --> 00:12:15,013 last point here and so the meaning that the judgments only holds on the assumption 135 00:12:15,013 --> 00:12:18,740 that the, that the expression actually completes.