#1Operational SemanticsOperational Semantics#2One-Slide Summary• Operational semantics are a precise way of specifying how to evaluate a program. •A formal semantics tells you what each expression means. •Meaning depends on context: a variable environment will map variables to memory locations and a store will map memory locations to values.#3Lecture Outline: OpSem• Motivation• Notation•The Rules– Simple Expressions– while– new– dispatch#4Motivation• We must specify for every Cool expression what happens when it is evaluated– This is the meaning of an expression•The definition of a programming language:– The tokens ⇒ lexical analysis– The grammar ⇒ syntactic analysis– The typing rules ⇒ semantic analysis–The evaluation rules ⇒ interpretation(also: hints for compilation)#5Evaluation Rules So Far• So far, we specified the evaluation rules intuitively–We described how dynamic dispatch behaved in words (e.g., “just like Java”)– We talked about scoping, variables, arithmetic expressions (e.g., “they work as expected”) • Why isn’t this description good enough?#6Assembly Language Description of Semantics• We might just tell you how to compile it– (but that would be helpful ...)•But assembly-language descriptions of language implementation have too many irrelevant details– Which way the stack grows– How integers are represented on a particular machine– The particular instruction set of the architecture•We need a complete but not overly restrictive specification#7Programming Language Semantics• There are many ways to specify programming language semantics•They are all equivalent but some are more suitable to various tasks than others•Operational semantics–Describes the evaluation of programs on an abstract machine–Most useful for specifying implementations– This is what we will use for Cool#8Other Kinds of Semantics • Denotational semantics – The meaning of a program is expressed as a mathematical object– Elegant but quite complicated• Axiomatic semantics– Useful for checking that programs satisfy certain correctness properties •e.g., that the quick sort function sorts an array– The foundation of many program verification systems#9Introduction to Operational Semantics• Once again we introduce a formal notation– Using logical rules of inference, just like typing•Recall the typing judgmentContext ` e : T(in the given context, expression e has type T)•We try something similar for evaluationContext ` e : v(in the given context, expression e evaluates to value v)#10Example Operational SemanticsInference Rule• In general the result of evaluating an expression depends on the result of evaluating its subexpressions•The logical rules specify everything that is needed to evaluate an expressionContext ` e1 + e2 : 12Context ` e1 : 5Context ` e2 : 7#11Aside• The operational semantics inference rules for Cool will become quite complicated– i.e., many hypotheses• This may initially look daunting•Until you realize that the opsem rules specify exactly how to build an interpreter•That is, every rule of inference in this lecture is pseudocode for an interpreter– So walking through the opsem (and thinking “I must generate code to implement this”) is a PA5 hint.#12• It might be tempting to protest this excursion into Theory• But I assert it will come in handy very soon!#13What Contexts Are Needed?• Contexts are needed to handle variables•Consider the evaluation of y à x + 1– We need to keep track of values of variables– We need to allow variables to change their values during the evaluation• We track variables and their values with:– An environment : tells us at what address in memory is the value of a variable stored– A store : tells us what is the contents of a memory location#14What Contexts Are Needed?• Contexts are needed to handle variables•Consider the evaluation of y à x + 1– We need to keep track of values of variables– We need to allow variables to change their values during the evaluation• We track variables and their values with:– An environment : tells us at what address in memory is the value of a variable stored– A store : tells us what is the contents of a memory locationRemind me – why do we need a separate store and e nvironment?Are those compiler notions?Which is static? Whichis dynamic?#15Variable Environments• A variable environment is a map from variable names to locations•Tells in what memory location the value of a variable is stored– Locations = Memory Addresses• Environment tracks in-scope variables only • Example environment:E = [a : l1, b : l2]•To lookup a variable a in environment E we write E(a)#16 Lost?• Environments may seem hostile and unforgiving•But soon they'll feel just like home!•Names ! Locations#17Stores• A store maps memory locations to values•Example store:S = [l1 ! 5, l2 ! 7]•To lookup the contents of a location l1 in store S we write S(l1)•To perform an assignment of 12 to location l1 we write S[12/l1]– This denotes a new store S’ such thatS’(l1) = 12 and S’(l) = S(l) if l ≠ l1#18• Avoid mistakes in your stores!•Locations ! Values#19Cool Values• All values in Cool are objects– All objects are instances of some class (the dynamic type of the object)•To denote a Cool object we use the notation X(a1 = l1, …, an = ln) where– X is the dynamic type of the object–ai are the attributes (including those inherited)–li are the locations where the values of attributes are stored#20Cool Values (Cont.)• Special cases (without named attributes)Int(5) the integer 5Bool(true) the boolean trueString(4, “Cool”) the string “Cool” of length 4•There is a special value void that is a member of all types– No operations can be performed on it– Except for the test isvoid– Concrete implementations might use NULL here#21Operational Rules of Cool• The evaluation judgment isso, E, S ` e : v, S’ read:– Given so the current value of the self object– And E the current variable environment– And S the current store– If the evaluation of e terminates then– The returned value is v– And the new store is S’#22Notes• The “result” of evaluating an expression is both a value and a new store•Changes to the store model side-effects–side-effects = assignments to variables•The variable environment does not change• Nor does