DOC PREVIEW
UMD CMSC 330 - Operational Semantics

This preview shows page 1-2 out of 7 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 7 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 7 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 7 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

CMSC 330: Organization ofProgramming LanguagesOperational SemanticsCMSC 330 2Introduction• 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 youcan 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 3Roadmap: Compilation of programGrammar:SAA  id = EE  T+E | TT  P * T | PP  id | n | (E)Program:X = 2 + 3Compilation:Push XPush 2Push 3Add top 2Assign top to secondPostorder:postfixX 2 3 + =(Rec Des) Parsing: ast=+32XProgram semantics:What does programmean?Is this correct?What is program supposed to do?CMSC 330 4Operational 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) isexecuted• We will briefly look at operational semantics– A program is defined by how you execute it on a mathematicalmodel of a machine– Operational semantics are easy to understand• We will look at a subset of OCaml as an exampleCMSC 330 5Roadmap: Semantics of a programGrammar:SAA  id = EE  T+E | TT  P * T | PP  id | n | (E)Program:X = 2 + 3Compilation:Push XPush 2Push 3Add top 2Assign top to secondPostorder:postfixX 2 3 + =(Rec Des) Parsing: ast=+32XvalueProgram semantics:=+32XCMSC 330 6Evaluation• We’re going to define a relation E →v– This means “expression E evaluates to v”• So we need a formal way of defining programsand 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 vCMSC 330 7OCaml 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 confusionlaterCMSC 330 8Values• 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 differencebetween 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 toremember which is whichCMSC 330 9Grammars for Trees• We’re just using grammars to describe treesE ::= x | n | true | false | [] | if E then E else E | fun x = E | E Ev ::= n | true | false | [] | v::vtype value = Val_Num of int | Val_Bool of bool | Val_Nil | Val_Pair of value * valuetype ast = Id of string | Num of int | Bool of bool | Nil | If of ast * ast * ast | Fun of string * ast | App of ast * astGiven a program, we sawlast time how to convertit to an ast (e.g.,recursive descent parsing)Goal: For any ast, we want an operational ruleto obtain a value that represents the executionof astCMSC 330 10Operational Semantics Rules• Each basic entity evaluates to thecorresponding valuen →ntrue →truefalse →false[] →[]CMSC 330 11Operational 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 themathematical sum; the left-hand side is source code– But what about + (+ 3 4) 5 ?• We need recursion( + ) n m →n + mCMSC 330 12Rules 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 + mE1 →n E2 →mCMSC 330 13Error Cases• Because we wrote n, m in the hypothesis, we mean thatthey 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 theexpression is erroneous– A program that evaluates to a stuck expression produces a runtime error in practice+ E1 E2 →n + mE1 →n E2 →mCMSC 330 14Trees of Semantic Rules• When we apply rules to an expression, weactually get a tree– Corresponds to the recursive evaluation procedure• For example: + (+ 3 4 ) 5+ ( + 3 4) 5 →(+ 3 4) → 5 →3 → 4 →7 3 4512CMSC 330 15Rules for If• Examples– if false then 3 else 4 → 4– if true then 3 else 4 → 3• Notice that only one branch is evaluatedif E1 then E2 else E3 →E1 →true E2 →vvif E1 then E2 else E3 →E1 →false E3 →vvCMSC 330 16Rule 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 →v1E2 →v2v1::v2CMSC 330 17Rules for Hd and Tlhd E →E → v1::v2v1tl E →E →v1::v2v2CMSC 330 18Rules for Identifiers• Let’s assume for now that the only identifiersare parameter names– Ex. (fun x = + x 3) 4– When we see x in the body, we need to look it up– So we need to keep some sort of environment• This will be a map from identifiers to valuesx →???CMSC 330 19Semantics with Environments• Extend rules to the form A; E →v– Means in environment A, the program text E evaluates to v• Notation:– We write •for the empty environment– We write A(x) for the value that x maps to in A– We write A, x:v for the same environment as A, except x is now v• x might or might not have mapped to anything in A– We write A, A' for the environment with the bindings of A' added toand overriding the bindings of A– The empty environment can be omitted when things are clear,


View Full Document

UMD CMSC 330 - Operational Semantics

Documents in this Course
Exam #1

Exam #1

6 pages

Quiz #1

Quiz #1

2 pages

Midterm 2

Midterm 2

12 pages

Exam #2

Exam #2

7 pages

Ocaml

Ocaml

7 pages

Parsing

Parsing

38 pages

Threads

Threads

12 pages

Ruby

Ruby

7 pages

Quiz #3

Quiz #3

2 pages

Threads

Threads

7 pages

Quiz #4

Quiz #4

2 pages

Exam #2

Exam #2

6 pages

Exam #1

Exam #1

6 pages

Threads

Threads

34 pages

Quiz #4

Quiz #4

2 pages

Threads

Threads

26 pages

Exam #2

Exam #2

9 pages

Exam #2

Exam #2

6 pages

Load more
Download Operational Semantics
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Operational Semantics and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Operational Semantics 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?