Syntax of a Simple Imperative Language Small-step operational semantics Operational semantics Big-step operational semantics Small-step SOS for expression evaluation It is important to note that the order of evaluation is fixed by the small-step semantics. (e1,o）→(e1,o） (e2,o）→(e2,o) (e1+e2,）→(e+e2,o) (n+e2,o）→(n+e2,o) It is different from the following. (e2,σ）→(e5,σ) (e1,c）→(e1,σ) (e1+e2,r)→(e1+e%,o) (e1+n,o）→(e1+n,o) Next:subtraction. Operabonal Semantics
Syntax of a Simple Imperative Language Operational semantics Small-step operational semantics Big-step operational semantics Small-step SOS for expression evaluation It is important to note that the order of evaluation is fixed by the small-step semantics. (e1, σ) −→ (e 0 1 , σ) (e1 + e2, σ) −→ (e 0 1 + e2, σ) (e2, σ) −→ (e 0 2 , σ) (n + e2, σ) −→ (n + e 0 2 , σ) It is different from the following. (e2, σ) −→ (e 0 2 , σ) (e1 + e2, σ) −→ (e1 + e 0 2 , σ) (e1, σ) −→ (e 0 1 , σ) (e1 + n, σ) −→ (e1 + n, σ) Next: subtraction. Operational Semantics
Syntax ot a Simple Imperative Language Smal-step operational semantics Operational semantics Big-step operational semantics Small-step SOS for expression evaluation Transitions for subtraction: (e1,0）→(e,o) (e2,）→(e3,o) (e1-e2,c）→(e1-e2,r) (n-e2,c）→(n-e2,o) LnJL-」n2J=n (n1-n2,o）→(n,σ) Next:variables. Operatonal Semantics
Syntax of a Simple Imperative Language Operational semantics Small-step operational semantics Big-step operational semantics Small-step SOS for expression evaluation Transitions for subtraction: (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, σ) Next: variables. Operational Semantics
Syntax of a Simple Imperative Language Small-step operational semantics Operational semantics Big-step operational semantics Small-step SOS for expression evaluation Recall (State)σ∈Var→Values Transitions for evaluating variables: (x)=[n] (x,o）→(n,o) Operational Semantics
Syntax of a Simple Imperative Language Operational semantics Small-step operational semantics Big-step operational semantics Small-step SOS for expression evaluation Recall (State) σ ∈ Var → Values Transitions for evaluating variables: σ(x) = bnc (x, σ) −→ (n, σ) Operational Semantics
Syntax ot a Simple Imperative Language Small-step operational semantics Operational semantics Big-step operational semantics Summary:small-step SOS for expression evaluation (e1,）→(e,) (e2,)→(e3,) (e1+e2,）→(e+e2,o) (n+e2,σ)→(n+e2,) (e1,o）→(e,) (e2,）-→(e,c) (e1-e2,o)-→(e1-e2,σ） (n-e2,）-→(n-e2,o) ln」L+」Ln2」=n n」L-Ln2」=n) a(x)=[n] (n1+2,）-→(n,c) (n1-n2,o）→(n,) (x,）-→(n, Example:Suppose (x)=10 and (y)=42. (x+y,0）→(10+y,)→(10+42,0)→(52，σ） Operatonal Semantics
Syntax of a Simple Imperative Language Operational semantics Small-step operational semantics Big-step operational semantics Summary: small-step SOS for expression evaluation (e1, σ) −→ (e 0 1 , σ) (e1 + e2, σ) −→ (e 0 1 + e2, σ) (e2, σ) −→ (e 0 2 , σ) (n + e2, σ) −→ (n + e 0 2 , σ) (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, σ) bn1c b−c bn2c = bnc (n1 − n2, σ) −→ (n, σ) σ(x) = bnc (x, σ) −→ (n, σ) Example: Suppose σ(x) = 10 and σ(y) = 42. (x + y, σ) −→ (10 + y, σ) −→ (10 + 42, σ) −→ (52, σ) Operational Semantics
Syntax of a Simple Imperative Language Small-step operational semantics Operational semantics Big-step operational semantics Small-step SOS for boolean expressions Recall (BoolExp)b ::true false I e=ele<e l e>e Ib Ibb l b vb l... We overload the symbol-. Transitions for comparisons: (e1,σ）→(e1,o) (e2,σ)→(e2,c) (e1=e2,o）→(e{=e2,o） (n=e2,o)→(n=e2,0) Ln」L=JLn2J -(Ln1」L=」Ln2J) (n1=n2,）→(true,σ) (n1=n2,o）→(false,σ) Next:negation. Operational Semantics
Syntax of a Simple Imperative Language Operational semantics Small-step operational semantics Big-step operational semantics Small-step SOS for boolean expressions Recall (BoolExp) b ::= true | false | e = e | e < e | e > e | ¬b | b ∧ b | b ∨ b | . . . We overload the symbol −→. Transitions for comparisons: (e1, σ) −→ (e 0 1 , σ) (e1 = e2, σ) −→ (e 0 1 = e2, σ) (e2, σ) −→ (e 0 2 , σ) (n = e2, σ) −→ (n = e 0 2 , σ) bn1c b=c bn2c (n1 = n2, σ) −→ (true, σ) ¬(bn1c b=c bn2c) (n1 = n2, σ) −→ (false, σ) Next: negation. Operational Semantics