南京大学：《程序设计语言的形式语义》课程教学资源（课件讲稿）05_Operational Semantics

Syntax ot a Simple Imperative Language Operational semantcs Operational Semantics Operabonal Semantics

Syntax of a Simple Imperative Language Operational semantics Operational Semantics Operational Semantics

Syntax of a Simple Imperative Language Operational semantics A programming language o Syntax o Semantics Operational Semantics

Syntax of a Simple Imperative Language Operational semantics A programming language Syntax Semantics Operational Semantics

Syntax ot a Simple Imperative Language Operational semantics Formal semantics of a programming language o Operational semantics o Denotational semantics o Axiomatic semantics Operatonal Semantics

Syntax of a Simple Imperative Language Operational semantics Formal semantics of a programming language Operational semantics Denotational semantics Axiomatic semantics Operational Semantics

Syntax of a Simple Imperative Language Operational semantics Operational semantics Operational semantics defines program executions: o Sequence of steps,formulated as transitions of an abstract machine Configurations of the abstract machine include: o Expression/statement being evaluated/executed o States:abstract description of registers,memory and other data structures involved in computation Operational Semantics

Syntax of a Simple Imperative Language Operational semantics Operational semantics Operational semantics defines program executions: Sequence of steps, formulated as transitions of an abstract machine Configurations of the abstract machine include: Expression/statement being evaluated/executed States: abstract description of registers, memory and other data structures involved in computation Operational Semantics

Syntax ot a Simple Imperative Language Cperational semantics Program Abstract Machine Input Function Initial Configuration Inputs Intermediate Configuration Rules Intermediate Configuration Auswer Output Function Final Configuration Figure taken from Franklyn Turbak and David Gifford's Design Concepts in Programming Languages. Operatonal Semantics

Syntax of a Simple Imperative Language Operational semantics Figure taken from Franklyn Turbak and David Gifford’s Design Concepts in Programming Languages. Operational Semantics

Syntax of a Simple Imperative Language Operational semantics Different approaches of operational semantics oSmall-step semantics: Describe each single step of the execution o Big-step semantics: Describe the overall result of the execution We will explain both in detail by examples Operational Semantics

Syntax of a Simple Imperative Language Operational semantics Different approaches of operational semantics Small-step semantics: Describe each single step of the execution Big-step semantics: Describe the overall result of the execution We will explain both in detail by examples. Operational Semantics

Syntax ot a Simple Imperative Language Operational semantics After this class... You should be able to: o write down the evaluation/execution steps,if given the operational semantics rules o formulate the operational semantics rule,if given the informal meaning of an expression/statement Operatonal Semantics

Syntax of a Simple Imperative Language Operational semantics After this class... You should be able to: write down the evaluation/execution steps, if given the operational semantics rules formulate the operational semantics rule, if given the informal meaning of an expression/statement Operational Semantics

Syntax of a Simple Imperative Language Operational semantics Outline Syntax of a Simple Imperative Language 2 Operational semantics o Small-step operational semantics oStructural operational semantics(SOS) o Extensions:going wrong,local variable declaration,heap o Contextual semantics (a.k.a.reduction semantics) Big-step operational semantics Operational Semantics

Syntax of a Simple Imperative Language Operational semantics Outline 1 Syntax of a Simple Imperative Language 2 Operational semantics Small-step operational semantics Structural operational semantics (SOS) Extensions: going wrong, local variable declaration, heap Contextual semantics (a.k.a. reduction semantics) Big-step operational semantics Operational Semantics

Syntax of a Simple Imperative Language Operational semantics Syntax (IntExp)e ::n x I e+e l e-e l... (BoolExp)b ::true I false I e=elee b bAb lbvb l... (Comm)c ::skip |X:=e C;C if b then c else c I while b do c Operatonal Semantics

Syntax of a Simple Imperative Language Operational semantics Syntax (IntExp) e ::= n | x | e + e | e − e | . . . (BoolExp) b ::= true | false | e = e | e e | ¬b | b ∧ b | b ∨ b | . . . (Comm) c ::= skip | x := e | c ; c | if b then c else c | while b do c Operational Semantics

Syntax of a Simple Imperative Language Operational semantics Syntax (IntExp)e ::n I x I e+e l e-e l... Here n ranges over the numerals 0,1,2,.... We distinguish between numerals,written n,0,1,2,...,and the natural numbers,written n,0,1,2,....The natural numbers are the normal numbers that we use in everyday life,while the numerals are just syntax for describing these numbers. We write Ln]to denote the meaning of n.We assume that Ln]=n, l0=0,l1J=1,.. The distinction is subtle,but important,because it is one manifestation of the difference between syntax and semantics. Operational Semantics

Syntax of a Simple Imperative Language Operational semantics Syntax (IntExp) e ::= n | x | e + e | e − e | . . . Here n ranges over the numerals 0, 1, 2, . . . . We distinguish between numerals, written n, 0, 1, 2, . . . , and the natural numbers, written n, 0, 1, 2, . . . . The natural numbers are the normal numbers that we use in everyday life, while the numerals are just syntax for describing these numbers. We write bnc to denote the meaning of n. We assume that bnc = n, b0c = 0, b1c = 1, . . . . The distinction is subtle, but important, because it is one manifestation of the difference between syntax and semantics. Operational Semantics