In this video we're going to begin our
discussion of formal operational semantics
Just as we did with lexical analysis,
parsing and type-checking. The first step
in defining what we mean by a formal
operational semantics is introduced the
notation and it turns out that the
notation we want to use for operational
semantics is the same or very similar in
the notation we use in type-checking. We
are going to be using logical rule of
inference. So, in the case of
type-checking, the kinds of inference
rules we, we presented, proofing's of the
forms that in some context. We could show
that some expression had a particular type
in this case to type c. And for evaluation
we're going to be doing something quite
similar. We will show that in some
contacts now that this is going to be a
different kind of context that we had in
typing so this is going to be an
evaluation context as oppose to a type
context and so what goes in the context
will actually be different. But for the
moment all that really matters is there is
some kind of a context and in that context
we're going to be able to show some
expression evaluates to a particular value
b. So as an example, let's take a look at
this simple expression, e1 + e2 and let's
say that using our rules which we, I
haven't shown you yet, but let's say we
had a bunch of rules and we could show in
the initial context. That e1 in that same
context, okay? So these context are going
to be the same, that e1 evaluated to the a
value of five and e2 also in that same
context evaluated to the value of, of
seven then we could prove that e1 + e2
evaluated to the value of twelve. If you
think about it what this rule was saying
is that if e1 evaluates to five and e2
evaluates to seven, then if you evaluated
the expression e1 + e2, you're going to
get the value twelve. And what's the
context doing, well it doesn't do a whole
lot in this particular rule. But remember
what the context was for in type checking.
The context was for giving values to the
free variables of the expression. And so,
we need for an expres sion like e1 + e2 to
say something about what the values are,
the variable that might appear in e1 and
in e2 in order to say what they evaluate
to and, and therefore, to say what the
entire expression e1 + e2 will evaluated
to. Now, let's be a little more precise
about what's going to go in the context.
So, let's consider the evaluation of a, a
expression or statement like y gets x+1.
Okay, so we are going to assign y the
value x+1 and there are two things that we
have to know in order to evaluate this
expression. First of all, we have to know
where In memory of valuable start. So, for
example, the variable x here, we're going
to have to go and look up excess value and
then add one to it And then that value is
going to be stored in whatever memory
location holds the value for y okay so
there is a mapping from variables, Two
memory locations. Okay and that is called,
In operational semantics the environment
and this is a little confusing maybe
because it use environment for other
things. Okay, so now let's forget about,
as all we uses of the word environment. We
were talking about the operational
semantics, what the environment means is
the mapping, the association in between
variables and where that variable store in
memory. And then in addition, we're going
to need a store and that's going to tell
us what is in the memory. So just knowing
the location for a variable isn't quite
enough. When we, if we know the value of x
if we know the location for x, for example
or as, as important because we're going to
get the value of x but we also have to
know exactly when value is stored there
and so store. Is going to be a mapping for
memory locations Values. These are the
values that are actually stored in the
memory so it's two levels of mapping. We
associate with each variable and memory
location And then each memory location
will have a value in it. So let's talk
about the notation that we're going to use
for writing down the environment and the
store. So as we said, the variable
environments have variables to locations
and we're going to w rite that out. In the
following way, we're going to just have
this as a list of variables and location
pairs separated by columns and this
environment for examples of variable a, is
it location l1 And variable b is in
location l2. And another aspect of the
environment is that it's going to keep
track of the variables that are in scalps
and the only variables that will be
mentioned in the environment are those
currently in sculpted in the expression
that is being evaluated. Now as we said,
stores map memory location to values and
we'll also write out stores as lists of
pairs. So in this case, the memory
location l1 in the store contains the
value five and the memory location l2
contains the value seven And we will also
separate these pairs by an arrow. And just
to make the stores look a little bit
different from the environment so that we
won't confuse the two. There's an
operation on stores which is to replace of
value or update of value. So, in this
case, we're taking the store s and we're
updating the value at location l1 to b12
And this defines a new store s prime. So,
keep in mind here that the stores are just
functions list in our model and so we can
define a new store by taking the old
function or the old store has and
modifying it at one point. So this defines
a new store as prime such if I apply s
prime to the location l1, I get off the
new value twelve and if I apply s prime to
any other location, any location different
from l1 I get out the value that the store
held in s, sorry the value of the location
in store s. Now in Cool we have more
complicated values and integers. In
particular we have objects and all the
objects of course are instances of some
class and we're going to need a notation
for representing objects in our
operational semantics. So we'll use the
following way of writing down an object.
An object will begin with its class name.
In this case the class name x and it would
be followed by a list of the attributes.
In this case the class x has n attributes,
a1 through an And associated with each
attribute will be the memory location
whether an attribute stored so attribute
a1 is stored location l1 up through
attribute and which is stored at location
ln. And this would be a complete
description of the object because we know
where in memory the object the object is
stored. We can use the store to look up
the value of each of those attributes.
There are few special classes in Kuhl that
don't have attribute names and we'll have
special way overriding them. So integers
only have a value and, and that will be
written as int with a single value in
parens, the value of the integer similarly
for brilliance. They have a single value
true of false and strings have two
properties, the length of the string and
the sting constant. There's also a special
value void typed object and we'll use the
term void in our operational semantics to
representative and briefly here, so void
is a, a special and that there are no
operations that can be before and on void
except for the test is void. So, in
particular, you can't dispatch the void
even though it has typed objects that will
generate runtime error. The only thing you
can do is to test whether the value is
void or not. And concrete implementation
we typically use a null pointer which
represent void. Now we're ready to talk
about in more detail what the judgments
will look like in our operational
semantics so the context will consist of
three pieces. The first piece is a current
self object. The second piece is the
environment which is again the mapping
from variables to the locations where
those variables are stored and the third
piece is the memory, the store. The
mapping from memory locations to the
values held at those locations, All right?
So in some context, an expression e will
evaluate to two things. First of all, e
will produce a value so for example we saw
before that the expressions seven + five
would produce the value twelve, that's one
result to the evaluation. But the second
thing is that we'll produce a modified
store. So the expression e maybe a
complicated piece of code Maybe a whole
program is on the right and it might have
a slight statements that update the
contents of the memory And so, after e is
evaluated, there will be a new memory
state that we have to represent and so s
prime here represents the state of memory
after evaluation And now, those are couple
of things here. First of all the current
self object and the environment don't
change. They are not changed by evaluation
so which object is the self parameter to
the current method and. Well, the mapping
between variables and memory locations
that is not modified by running a, running
an expression and that makes sense, I
mean, you can't update the self object in
Kuhl and we don't have access in, in any
form to re-locations or variables stored
and so those two things are in variant.
They don't they are variant under
evaluation. They don't change when you run
a piece of code. However, the story does
change so the contents in the memory may
be modified so that's why we need a store
for both before evaluation and after
evaluation. And one more detail these
judgments of this form always has a
qualification. That judgment only holds if
the evaluation of e terminates. So, if e
goes in to infinite loop, then you're not
going to get a value and you're not going
to get a new store. So, this kind of the
judgment must always be read as saying
that if e terminates, then e produces a
value v and a new store s prime. Summarize
the results of evaluation is a value and a
new store. And where the new store models,
the side effects of the expression And
once again there are something don't
change as a result of evaluation. And this
is actually important for compilation
because we'll be able to take advantage of
the fact that they don't change to
generate efficient code so the variable
environment doesn't change, the value
itself which object we're talking about
doesn't change and notice here as another
detail. That the contents of the self
objects, the attributes inside the self
object might change, they might get
updated but t he locations where the
attributes are stored do not change. So,
the layout of the object where the object
stored doesn't change and that's all we're
saying here, the actual contents of the
object which of course is a part of the
mapping of the store, those might get
updated by evaluation. And also the
operational semantics allows for
non-terminating evaluations. That's the
last point here and so the meaning that
the judgments only holds on the assumption
that the, that the expression actually
completes.