CMSC 330: Organization of Programming Languages Operational Semantics CMSC 330 2 Introduction •! So far we’ve looked at regular expressions, automata, and context-free grammars –! These are ways of defining sets of strings –! We can use these to describe what programs you can write down in a language •! (Almost...) –! I.e., these describe the syntax of a language •! What about the semantics of a language? –! What does a program “mean”? CMSC 330 3 Roadmap: Compilation of program Grammar: S!A A ! id = E E ! T+E | T T ! P * T | P P ! id | n | (E) Program: X = 2 + 3 Compilation: Push X Push 2 Push 3 Add top 2 Assign top to second Postorder: postfix X 2 3 + = (Rec Des) Parsing: ast = + 3 2 X Program semantics: What does program mean ? Is this correct? What is program supposed to do? CMSC 330 4 Operational Semantics •! There are several different kinds of semantics –! Denotational: A program is a mathematical function –! Axiomatic: Develop a logical proof of a program •! Give predicates that hold when a program (or part) is executed •! We will briefly look at operational semantics –! A program is defined by how you execute it on a mathematical model of a machine –! Operational semantics are easy to understand •! We will look at a subset of OCaml as an exampleCMSC 330 5 Roadmap: Semantics of a program Grammar: S!A A ! id = E E ! T+E | T T ! P * T | P P ! id | n | (E) Program: X = 2 + 3 Compilation: Push X Push 2 Push 3 Add top 2 Assign top to second Postorder: postfix X 2 3 + = (Rec Des) Parsing: ast = + 3 2 X value Program semantics: = + 3 2 X CMSC 330 6 Evaluation •! We’re going to define a relation E ! v –! This means “expression E evaluates to v” •! So we need a formal way of defining programs and of defining things they may evaluate to •! We’ll use grammars to describe each of these –! One to describe abstract syntax trees E –! One to describe OCaml values v CMSC 330 7 OCaml Programs •! E ::= x | n | true | false | [] | if E then E else E | fun x = E | E E –! x stands for any identifier –! n stands for any integer –! true and false stand for the two boolean values –! [] is the empty list –! Using = in fun instead of -> to avoid some confusion later CMSC 330 8 Values •! v ::= n | true | false | [] | v::v –! n is an integer (not a string corresp. to an integer) •! Same idea for true, false, [] –! v1::v2 is the pair with v1 and v2 •! This will be used to build up lists •! Notice: nothing yet requires v2 to be a list –! Important: Be sure to understand the difference between program text S and mathematical objects v. •! E.g., the text 3 evaluates to the mathematical number 3 –! To help, we’ll use different colors and italics •! This is usually not done, and it’s up to the reader to remember which is whichCMSC 330 9 Grammars for Trees •! We’re just using grammars to describe trees E ::= x | n | true | false | [] | if E then E else E | fun x = E | E E v ::= n | true | false | [] | v::v type value = Val_Num of int | Val_Bool of bool | Val_Nil | Val_Pair of value * value type ast = Id of string | Num of int | Bool of bool | Nil | If of ast * ast * ast | Fun of string * ast | App of ast * ast Given a program, we saw previously how to convert it to an ast (e.g., recursive descent parsing) Goal: For any ast, we want an operational rule to obtain a value that represents the execution of ast CMSC 330 10 Operational Semantics Rules •! Each basic entity evaluates to the corresponding value n ! n true ! true false ! false [] ! [] CMSC 330 11 Operational Semantics Rules (cont’d) •! How about built-in functions? –! We’re applying the + function •! (we put parens around it because it’s not in infix notation; will skip this from now on) •! Ignore currying for the moment, and pretend we have multi-argument functions –! On the right-hand side, we’re computing the mathematical sum; the left-hand side is source code –! But what about + (+ 3 4) 5 ? •! We need recursion ( + ) n m ! n + m CMSC 330 12 Rules with Hypotheses •! To evaluate + E1 E2, we need to evaluate E1, then evaluate E2, then add the results –! This is call-by-value –! This is a “natural deduction” style rule –! It says that if the hypotheses above the line hold, then the conclusion below the line holds •! i.e., if E1 executes to value n and if E2 executes to value m, then + E1 E2 executes to value n+m + E1 E2 ! n + m E1 ! n E2 ! mCMSC 330 13 Error Cases •! Because we wrote n, m in the hypothesis, we mean that they must be integers •! But what if E1 and E2 aren’t integers? –! E.g., what if we write + false true ? –! It can be parsed, but we can’t execute it •! We will have no rule that covers such a case –! Convention: If there is not rule to cover a case, then the expression is erroneous –! A program that evaluates to a stuck expression produces a run time error in practice + E1 E2 ! n + m E1 ! n E2 ! m CMSC 330 14 Trees of Semantic Rules •! When we apply rules to an expression, we actually get a tree –! Corresponds to the recursive evaluation procedure •! For example: + (+ 3 4 ) 5 + ( + 3 4) 5 ! (+ 3 4) ! 5 ! 3 ! 4 ! 7 3 4 5 12 CMSC 330 15 Rules for If •! Examples –! if false then 3 else 4 ! 4 –! if true then 3 else 4 ! 3 •! Notice that only one branch is evaluated if E1 then E2 else E3 ! E1 ! true E2 ! v v if E1 then E2 else E3 ! E1 ! false E3 ! v v CMSC 330 16 Rule for :: •! So :: allocates a pair in memory •! Are there any conditions on E1 and E2? –! No! We will allow E2 to be anything –! OCaml’s type system will disallow non-lists :: E1 E2 ! E1 ! v1 E2 ! v2 v1::v2CMSC 330 17 Rules for Hd and …
View Full Document
Unlocking...