1CMSC 330:Operational Semantics2IntroductionWe’ve looked at several formal methods for defining the syntax of a programming language•Regular expressions•Context-free grammarsWhat about formal methods for defining the semantics of a programming language?•I.e., what does a program mean?3Roadmap: Compilation of ProgramGrammar:SAA id = EE T+E | TT P * T | PP id | n | (E)Program:X = 2 + 3Compilation:Push XPush 2Push 3Add top 2Assign top tosecondPostorder:postfixX 2 3 + =Recursive Descent Parsing: AST=+32XProgram semantics:What does program mean?Is this correct?What is program supposed to do?4Formal SemanticsFormal semantics of a programming language•Mathematical model of all possible computations performed by programs written in that languageThree main approaches to formal semantics•Denotational•Operational•Axiomatic5Formal Semantics (cont.)Denotational semantics•Translate parts of language into another languageUsually a mathematical functionMeaning of program expressed as mathematical objectOperational semantics•Describe effect of parts of languageUsually on (a mathematical model of) an abstract machineFor lambda calculus, can use syntactic transformationsAxiomatic semantics•Describe each part of language through logical axiomsFoundation of many program verification systems6Operational SemanticsWe will briefly look at operational semantics•Using a subset of OCaml as an exampleUseful for•Specifying the meaning of a program•Proving the correctness of an algorithmThrough formal verificationFor cryptographic algorithms, combinatorial circuits, etc…Currently limited to smaller programs7Roadmap: Semantics of a ProgramGrammar:SAA id = EE T+E | TT P * T | PP id | n | (E)Program:X = 2 + 3Compilation:Push XPush 2Push 3Add top 2Assign top tosecondPostorder:postfixX 2 3 + =Recursive Descent Parsing: AST=+32XvalueProgram Semantics:=+32X8EvaluationWe’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 toWe’ll use grammars to describe each of these•One to describe abstract syntax trees E•One to describe OCaml values v9OCaml ProgramsE ::= 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 later10Valuesv ::= 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 v2This will be used to build up listsNotice: nothing yet requires v2 to be a list•Important: Be sure to understand the difference between program text S and mathematical objects vE.g., the text 3 evaluates to the mathematical number 3•To help, we’ll use different colors and italicsIf not present, it’s up to you to remember which is which11Grammars for TreesWe’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 know how to convert it to an AST using recursive descent parsingGoal: For any AST, we want an operational rule to obtain a value that represents the execution of that AST12Operational Semantics RulesEach basic entity evaluates to its corresponding valuen → ntrue → truefalse → false[] → []13Operational Semantics Rules (cont.)How about built-in functions?•We’re applying the + functionWe put parens around it because it’s not in infix notation•Will skip this from now onIgnore currying for the moment•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 + m14Rules with HypothesesTo evaluate + E1E2, 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 holdsi.e., if E1executes to value n and if E2executes to value m, then + E1E2executes to value n+m+ E1E2→ n + mE1→ n E2→ m15Error CasesWhat if E1 and E2 aren’t integers?•E.g., what if we write + false true ?•It can be parsed, but we can’t execute itPrevious rule does not cover such a case•Because we wrote n, m in the hypothesisSo they must be integers Convention•If there is no rule to cover a caseThen the expression is erroneous•A program that evaluates to an erroneous expressionProduces a run-time error in practice+ E1E2→ n + mE1→ n E2→ m16Trees of Semantic RulesWhen we apply rules to an expression, we actually get a tree•Corresponds to the recursive evaluation procedureFor example: + (+ 3 4 ) 5+ ( + 3 4) 5 →(+ 3 4) → 5 →3 → 4 →73 451217Rules for IfExamples•if false then 3 else 4 →4•if true then 3 else 4 →3Notice that only one branch is evaluatedif E1then E2 else E3→E1→ true E2→ vvif E1then E2 else E3→E1→ false E3→ vv18Rule for ::So :: allocates a pair in memoryAre there any conditions on E1and E2?•No! We will allow E2to be anything•OCaml’s type system will disallow non-lists:: E1E2→E1→ v1E2→ v2v1::v219Rules for IdentifiersLet’s assume for now that the only identifiers are parameter names•Example: (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 environmentThis will be a map from identifiers to values20Semantics with EnvironmentsExtend rules to the form A; E → v•Means in environment A, program text E evaluates to vNotation•We write • for the empty environment (may be omitted)•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 xis now vx might or might not have mapped to anything in A•We write A, A' for the environment with the bindings of A'added to and overriding the bindings of A21Rules for Identifiers and ApplicationTo evaluate a user-defined function applied to an argument:•Evaluate the argument
View Full Document
Unlocking...