CSc 520Principles of Programming Languages52: Semantics — Operational SemanticsChristian CollbergDepartment of Computer ScienceUniversity of [email protected] 2005 Christian CollbergApril 22, 20051 Operational Semantics• In this lecture we will describe a method for the formal specification of programming languages, knownas structural operational semantics.• Operation semantics describes how a computation is performed.• We’ve already seen some operational semantic methods:1. A metacircular interpreter for Scheme,2. The β-reduction rule with the normal order reduction strategy for λ-calculus.2 Operational Semantics. . .• An operational semantics operates on a sequence of states.• We start with an initial state.• The program maps the initial state into a new state, and so on, until a final state is reached, the resultof the program.3 Operational Semantics — λ-calculus• A configuration consists of the lambda expression that’s left to reduce.• The transition function applies β and δ-reductions according to our evaluation strategy.• The evaluation terminates when a configuration is in normal form.14 Structural Operational Semantics• Operational semantics specifies the semantics of a language in terms of how it would be executed onan abstract machine.• In Structural Operational Semantics (SOS), definitions are given by inference rules.• SOS turns the abstract machine into a system of logical inferences.Inference Rules5 Inference Rules• Inference rules:premise1premise1· · · premisenconclusionThe conclusion follows from the premises.• Sometimes we add a condition under which the rule is applicable:premise1premise1· · · premisenconclusionCondition6 Inference Rules. . .• Sometimes there are no premises (this is called an axiom:conclusionin which case we omit the line:conclusion7 Inference Rules — Examples• Example from Natural Deduction (logical properties of conjunction (and)):p ∧ qpp ∧ qqp qp ∧ q• Example from Natural Deduction (introduction of universal quantifier):P (a)∀xP (x)a does not occur in P(x) or in any assumptionon which P(a) dependsAbstract Syntax of Wren28 Abstract Syntax• The operational semantics operates on a abstract syntax of the language.• The abstract syntax ignores the surface syntax and only specifies the “essential” parts of each languageconstruct.• We can use any convenient way to define the abstract syntax, EBNF, for example.• We use inference rules to specify the abstract syntax.• The next slide gives the types of objects that we use to construct the abstract syntax from.9 Syntactic Categoriesn ∈ Num = Set of numeralsb ∈ {true, false} = Set of Boolean valuesid ∈ Id = Set of integer identifiersbid ∈ Bid = Set of Boolean identifiersiop ∈ Iop = {+, −, ∗, /}rop ∈ Rop = {<, ≤, =, ≥, >, <>}bop ∈ Bop = {and, or}ie ∈ Iexp = Set of integer expressionsbe ∈ Bexp = Set of Boolean expressionsc ∈ Cmd = Set of commands10 Abstract Syntax — Integers• Objects from Num may serve as integer expressions:n : iexpn ∈ NumNote that this rule is an abbreviated form ofn : iexpn ∈ Num• Integer identifiers may serve as integer expressions:id : iexpid ∈ Id11 Abstract Syntax — Integers. . .• Integer unary/binary/relational expressions:ie1: iexp ie2: iexpie1iop ie2: iexpiop ∈ Iopie1: iexp ie2: iexpie1rop ie2: bexprop ∈ Ropie : iexp− ie : iexp• Remember thatiop ∈ Iop = {+, −, ∗, /}rop ∈ Rop = {<, ≤, =, ≥, >, <>}ie ∈ Iexp = Set of integer expressions312 Abstract Syntax — Booleans• Objects from Num may serve as boolean expressions:b : bexpb ∈ {true, false}• Boolean identifiers may serve as boolean expressions:bid : bexpbid ∈ Bid• Boolean binary expressions:be1: bexp be2: bexpbe1bop be2: bexpbop ∈ Bopbe : bexpnot be : bexp13 Abstract Syntax — Commandsskip : cmdie : iexpid := ie : cmdid ∈ Idbe : bexpbid := be : cmdbid ∈ Bidread id : cmdid ∈ Idie : iexpwrite ie : cmd14 Abstract Syntax — Commands. . .be : bexp c : cmdif be then c : cmdbe : bexp c1: cmd c2: cmdif be then c1else c2: cmdc1: cmd c2: cmdc1; c2: cmdbe : bexp c : cmdwhile be do c : cmd15 Abstract Syntax — Example• We can show that the following is a valid Wren command by derivingx:= 5 ; while not(x = 0) do x:= x − 1 ; write x : cmdx : iexp 0 : iexpx = 0 : bexpnot(x = 0) : bexpx : iexp 1 : iexpx − 1 : iexpx:= x − 1 : cmdwhile not(x = 0) do x:= x − 1 : cmd• The next slide shows the complete derivation.416 Abstract Syntax — Example. . .5 : iexpx:= 5 : cmdx : iexp 0 : iexpx = 0 : bexpnot(x = 0) : bexpx : iexp 1 : iexpx − 1 : iexpx:= x − 1 : cmdwhile not(x = 0) do x:= x − 1 : cmdx : iexpwrite x : cmdwhile not(x = 0) do x:= x − 1 ; write x : cmdx:= 5 ; while not(x = 0) do x:= x − 1 ; write x : cmdSemantics of Wren Expressions17 Semantics of Wren Expressions• SOS applies sequences of transformations to the abstract syntax of a program. Each step produces anew configuration.• Three things can happen:1. We arrive at a normal form configuration where no more transformations can be applied. Thisnormal form is the meaning of the program.2. Computation gets stuck in a configuration from which no more transformations are possible. Forexample, the program might try to divide-by-zero.3. We find ourselves in a non-terminating sequence of configurations.18 Store Abstract Data Type• Wren expressions can contain identifiers.• We model the set of identifiers available to an expression using a store abstraction.• The store is a set of pairssto = {x 7→ 3, y 7→ 5, p 7→ true}mapping identifiers to their bound values.• The domain of the store is the set of defined variables:dom(sto) = {x, y, z}19 Store Abstract Data Type. . .• emptySto is a store where all identifiers are undefined.• updateSto(sto, id, n) extends sto with a new binding id 7→ n.• applySto(sto, id) returns the value associated with id.5• For example, the store{x 7→ 3, y 7→ 5, p 7→ true}maps three variables to their respective values.• It would be created and queried like this:updateSto(updateSto(updateSto(emptySto, p, true), y, 5), x, 3)applySto({x 7→ 3, y 7→ 5, p 7→ true}, p) ⇒ true20 Configurations• In our inference system a configuration looks like this:hexpression, storei• expression is the expression we’re examining.• store is the context (set of identifiers) in which it should be evaluated.• In Wren, a final configuration (a
View Full Document
Unlocking...