Operational SemanticsCMSC 330, Spring 20111 IntroductionSo far in class, we’ve talked about different ways of specifying the syntax of programs, notably regularexpressions and context-free grammars. In this lecture, we will examine ways to describe the semantics ofprograms, i.e., what they mean.Many of today’s languages, such as C, C++, and Java, have semantics that are described by long,English-language documents. While this documentation is precise in some sense, it can be hard to knowwhether the semantics are• consistent —are there places in the language description that conflict with each other?;• sufficient—is every possible valid program assigned a meaning? For example, C leaves many aspectsof the language undefined.; and• correct—does the language do what programmers would expect?The situation is even worse with other languages, such as Ruby, Python, and Perl, that have no clearspecification other than their implementation.2 Kinds of Formal SemanticsIn contrast, we are going to study how to write down formal semantics for a programming language. Whileformality doesn’t directly address consistency, sufficiency, and correctness, it gives us a much better shot atthem. Formal semantics are concise, precise, and subject to formal reasoning, and so it’s a lot easier to besure they’re right; and if they’re not right, it’s easier to find the problems.There are three main approaches for describing formal semantics:• An axiomatic semantics of a program talks about how logical properties of the program state changeas a program runs. For example, if we know that currently x ≥ y ∧ z ≥ w, and the next statementin the program is a := x + z1, then after that statement we also know that a ≥ y + w. Axiomaticsemantics fell out of favor for a long time, but has seen recent re-popularity for tools that performanalysis of program source code. However, for purposes of this class, we will not discuss them further,since they are still hard to use; for example, explaining pointer-ful programs using axiomatic semanticsis an area of current research interest.• A denotational semantics of a program “compiles” programs into equivalent mathematical functionover something called a domain. Denotational semantics was developed by Dana Scott and Christo-pher Strachey, and was highly influential. However, denotational semantics requires sophisticatedmathematical reasoning, and it can be hard to use in practice.• An operational semantics of a program is essentially a program interpreter, written out in mathematicalnotation. Operational semantics is by far the most common way of describes semantics today, and itis what we will focus on in this lecture.1Here := is just ordinary assignment, written in a Pascal-style notation as is traditional in these semantics13 A Big-Step Operational SemanticsLanguage. We will define an operational semantics for the OCaml-like language given by the followinggrammar:e ::= x | n | true | false | e + e | if e then e else e | fun x → e | e eHere x represents an arbitrary variable, n is an integer, true and false are booleans, and if e1then e2else e3evaluates to e2if e1evaluates to true, and to e2if e1evaluates to false. Anonymous functions are createdwith fun x → e, and the expression e1e2calls function e1with argument e2.In OCaml terms, we can represent ASTs for the above language astype expr =EVar of string| ENum of int| ETrue| EFalse| EPlus of expr * expr| EIf of expr * expr * expr| EFun of string * expr| EApp of expr * exprwhere we use strings for the names of variables.Values and environments.v ::= n | true | false | (A, λx.e)A ::= ∅ | x : v, Atype value =VNum of int| VTrue| VFalse| VClosure of asst * string * exprand asst = (string * value) listSemantics rules.IntA ` n −→ nTrueA ` true −→ trueFalseA ` false −→ falseVarx ∈ dom(A)A ` x −→ A(x)PlusA ` e1−→ n A ` e2−→ m p = n+mA ` e1+ e2−→ pIf-TA ` e1−→ true A ` e2−→ vA ` if e1then e2else e3−→ vIf-FA ` e1−→ false A ` e3−→ vA ` if e1then e2else e3−→ vFunA ` fun x → e −→ (A, λx.e)AppA ` e1−→ (A0, λx.e) A ` e2−→ v2x : v2, A0` e −→ vA ` e1e2−→ v2let rec eval a = functionEVar x -> List.assoc x a| ENum n -> VNum n| ETrue -> VTrue| EFalse -> VFalse| EIf(e1, e2, e3) ->beginmatch eval a e1 withVTrue -> eval a e2| VFalse -> eval a e3end| EFun(x, e) -> VClosure(a, x, e)| EApp(e1, e2) ->let VClosure(a’, x, e) = eval a e1 inlet v2 = eval a e2 ineval ((x,v2)::a’) eExamples.eval [] (EPlus (ENum 3, ENum 4))eval [] (EIf(ETrue, ENum 3, ENum 4))eval [] (EIf(ETrue, (EPlus (ENum 3, ENum 4)), ENum 5))eval ["x", VNum 3] (EPlus (EVar "x", ENum 4))eval [] (EApp(EFun("x", EPlus (EVar "x", ENum 4)), ENum 3))eval [] (EApp(EApp(EFun("x", EFun("y", EPlus(EVar "x", EVar "y"))),ENum 3), ENum
View Full Document
Unlocking...