Syntax of a Simple Imperative Language Operational semantics Syntax Syntax Semantics L] (IntExp)e ::=n n x l e+e e-e (BoolExp)b = true true false false I e=e I e<e 1b A bvb Operatonal Semantics
Syntax of a Simple Imperative Language Operational semantics Syntax Syntax Semantics b·c (IntExp) e ::= n n | x | e + e + | e − e − | . . . (BoolExp) b ::= true true | false false | e = e = | e < e < | ¬b ¬ | b ∧ b ∧ | b ∨ b ∨ | . . . Operational Semantics
Syntax of a Simple Imperative Language Small-step operational semantics Operational semantics Big-step operational semantics States To evaluate variables or update variables,we need to know the current state. (State)σE Var-Values What are Values?n or n? Both are fine.Here we think Values are natural numbers,boolean values,etc. Operational Semantics
Syntax of a Simple Imperative Language Operational semantics Small-step operational semantics Big-step operational semantics States To evaluate variables or update variables, we need to know the current state. (State) σ ∈ Var → Values What are Values? n or n? Both are fine. Here we think Values are natural numbers, boolean values, etc. Operational Semantics
Syntax ot a Simple Imperative Language Small-step operational semantics Operational semantics Big-step operational semantics States (State)o E Var→Values For example,1=((x,2),(y,3),(a,10)1,which we will write as {x2,y3,a10}. (For simplicity,here we assume that a state always contain all the variables that may be used in a program.) Recall ifz≠x if z=x For example,oiy7)=(x2,y7,a10]. Operational semantics will be defined using configurations of the forms(e,σ，(b,σ）and(c,σ： Operatonal Semantics
Syntax of a Simple Imperative Language Operational semantics Small-step operational semantics Big-step operational semantics States (State) σ ∈ Var → Values For example, σ1 = {(x, 2),(y, 3),(a, 10)}, which we will write as {x { 2, y { 3, a { 10}. (For simplicity, here we assume that a state always contain all the variables that may be used in a program.) Recall σ{x { n} def = λz. ( σ(z) if z , x n if z = x For example, σ1{y { 7} = {x { 2, y { 7, a { 10}. Operational semantics will be defined using configurations of the forms (e, σ), (b, σ) and (c, σ). Operational Semantics
Syntax of a Simple Imperative Language Small-step operational semantics Operational semantics Bio-step operational semantics Small-step structural operational semantics(SOS) Systematic definition of operational semantics: o The program syntax is inductively-defined o So we can also define the semantics of a program in terms of the semantics of its parts o"Structural":syntax oriented and inductive Examples: o The state transition for e1+e2 is described using the transition for e and the transition for e2. o The state transition for c1;c2 is described using the transition for c and the transition for c2. Operatonal Semantics
Syntax of a Simple Imperative Language Operational semantics Small-step operational semantics Big-step operational semantics Small-step structural operational semantics (SOS) Systematic definition of operational semantics: The program syntax is inductively-defined So we can also define the semantics of a program in terms of the semantics of its parts “Structural”: syntax oriented and inductive Examples: The state transition for e1 + e2 is described using the transition for e1 and the transition for e2. The state transition for c1 ; c2 is described using the transition for c1 and the transition for c2. Operational Semantics
Syntax ot a Simple Imperative Language Smal-step operational semantics Operational semantics Big-step operational semantics Small-step SOS for expression evaluation Recall (IntExp)e ::n I x l e+e l e-e l... Below we define (e,)(e',').We'll start from addition. (e1,o)→(e,o) (e2,σ)→(e5,) (e1+e2,o）→(e{+e2,c) (n+e2,o）→(n+e2,o) LnJL+」Ln2」=Ln (n1+n2,c）→(n,) Example:(10+12)+(13+20),σ) Operatonal Semantics
Syntax of a Simple Imperative Language Operational semantics Small-step operational semantics Big-step operational semantics Small-step SOS for expression evaluation Recall (IntExp) e ::= n | x | e + e | e − e | . . . Below we define (e, σ) −→ (e 0 , σ0 ). We’ll start from addition. (e1, σ) −→ (e 0 1 , σ) (e1 + e2, σ) −→ (e 0 1 + e2, σ) (e2, σ) −→ (e 0 2 , σ) (n + e2, σ) −→ (n + e 0 2 , σ) bn1c b+c bn2c = bnc (n1 + n2, σ) −→ (n, σ) Example: ((10 + 12) + (13 + 20), σ) Operational Semantics