Programming Languages and Compilers (CS 421)Natural SemanticsPictureNatural Semantics of Atomic ExpressionsBooleans:RelationsArithmetic ExpressionsCommandsIf Then Else CommandWhile CommandExampleSlide 12Slide 13Slide 14Slide 15Slide 16Slide 17Slide 18Slide 19Slide 20Slide 21Slide 22Let in CommandSlide 24Slide 25CommentInterpretation Versus CompilationInterpreterInterpreterNatural Semantics ExampleSlide 31Why Have Both Semantics?Programming Languages and Compilers (CS 421)Elsa L Gunter2112 SC, UIUChttp://www.cs.uiuc.edu/class/fa06/cs421/Based in part on slides by Mattox Beckman, as updated by Vikram Adve and Gul AghaElsa L. Gunter Natural Semantics•Similar to transition semantics except–Transition semantics is relation between individual steps of computation–Natural semantics is relation between computation state and final result•Rules look like (C, m) m’•Always want Lemma: (C,m) -->* m’ iff (C, m) m’Elsa L. Gunter Picture •Transition semantics(C1,m1) --> (C2,m2) --> (C3,m3) --> … --> m•Natural Semantics (C1,m1) mElsa L. Gunter Natural Semantics of Atomic Expressions•Same as Transition •Identifiers: (I,m) m(I)•Numerals are values: (N,m) N•Booleans: (true,m) true (false ,m) falseElsa L. Gunter Booleans: (B, m) false (B, m) true (B’, m) b(B & B’, m) false (B & B’, m) b (B, m) true (B, m) false (B’, m) b(B or B’, m) true (B or B’, m) b(B, m) true (B, m) false(not B, m) false (not B, m) trueElsa L. Gunter Relations(E, m) U (E’, m) V U ~ V = b(E ~ E’, m) b•By U ~ V = b, we mean does (the meaning of) the relation ~ hold on the meaning of U and V•May be specified by a mathematical expression/equation or rules matching U and VElsa L. Gunter Arithmetic Expressions(E, m) U (E’, m) V U op V = N(E op E’, m) Nwhere N is the specified value for U op VElsa L. Gunter Commands(skip, m) m(E,m) V(I::=E,m) m[I <-- V ](C,m) m’ (C’,m’) m’’(C;C’, m) m’’Elsa L. Gunter If Then Else Command(B,m) true (C,m) m’(if B then C else C’ fi, m) m’(B,m) false (C’,m) m’(if B then C else C’ fi, m) m’Elsa L. Gunter While Command(B,m) false(while B do C od, m) m(B,m)true (C,m)m’ (while B do C od, m’)m’’(while B do C od, m) m’’Elsa L. Gunter Example (2,{x->7})2 (3,{x->7}) 3 (2+3, {x->7})5(x,{x->7}) 7 (5,{x->})5 (y:= 2 + 3, {x-> 7} (x > 5, {x -> 7})true {x- >7, y->5} (if x > 5 then y:= 2 + 3 else y:=3 + 4 fi, {x -> 7}) ?Elsa L. Gunter Example (2,{x->7})2 (3,{x->7}) 3 (2+3, {x->7})5(x,{x->7}) 7 (5,{x->})5 (y:= 2 + 3, {x-> 7} (x > 5, {x -> 7})? {x- >7, y->5} (if x > 5 then y:= 2 + 3 else y:=3 + 4 fi, {x -> 7}) ? {x->7, y->5}Elsa L. Gunter Example (2,{x->7})2 (3,{x->7}) 3 ? > ? = ? (2+3, {x->7})5(x,{x->7}) ? (5,{x->})? (y:= 2 + 3, {x-> 7} (x > 5, {x -> 7})? {x- >7, y->5} (if x > 5 then y:= 2 + 3 else y:=3 + 4 fi, {x -> 7}) ? {x->7, y->5}Elsa L. Gunter Example (2,{x->7})2 (3,{x->7}) 3 7 > 5 = true (2+3, {x->7})5(x,{x->7}) 7 (5,{x->})5 (y:= 2 + 3, {x-> 7} (x > 5, {x -> 7})? {x- >7, y->5} (if x > 5 then y:= 2 + 3 else y:=3 + 4 fi, {x -> 7}) ? {x->7, y->5}Elsa L. Gunter Example (2,{x->7})2 (3,{x->7}) 3 7 > 5 = true (2+3, {x->7})5(x,{x->7}) 7 (5,{x->})5 (y:= 2 + 3, {x-> 7} (x > 5, {x -> 7})true {x- >7, y->5} (if x > 5 then y:= 2 + 3 else y:=3 + 4 fi, {x -> 7}) ? {x->7, y->5}Elsa L. Gunter Example (2,{x->7})2 (3,{x->7}) 3 7 > 5 = true (2+3, {x->7})5(x,{x->7}) 7 (5,{x->})5 (y:= 2 + 3, {x-> 7} (x > 5, {x -> 7})true ? .(if x > 5 then y:= 2 + 3 else y:=3 + 4 fi, {x -> 7}) ? {x->7, y->5}Elsa L. Gunter Example (2,{x->7})2 (3,{x->7}) 3 7 > 5 = true (2+3, {x->7})?(x,{x->7}) 7 (5,{x->})5 (y:= 2 + 3, {x-> 7} (x > 5, {x -> 7})true ? {x- >7, y->5} (if x > 5 then y:= 2 + 3 else y:=3 + 4 fi, {x -> 7}) ? {x->7, y->5}Elsa L. Gunter Example ? + ? = ? (2,{x->7})? (3,{x->7}) ? 7 > 5 = true (2+3, {x->7})?(x,{x->7}) 7 (5,{x->})5 (y:= 2 + 3, {x-> 7} (x > 5, {x -> 7})true ? .(if x > 5 then y:= 2 + 3 else y:=3 + 4 fi, {x -> 7}) ? {x->7, y->5}Elsa L. Gunter Example 2 + 3 = 5 (2,{x->7})2 (3,{x->7}) 3 7 > 5 = true (2+3, {x->7})?(x,{x->7}) 7 (5,{x->})5 (y:= 2 + 3, {x-> 7} (x > 5, {x -> 7})true ?{x->7, y->5} (if x > 5 then y:= 2 + 3 else y:=3 + 4 fi, {x -> 7}) ? {x->7, y->5}Elsa L. Gunter Example 2 + 3 = 5 (2,{x->7})2 (3,{x->7}) 3 7 > 5 = true (2+3, {x->7})5(x,{x->7}) 7 (5,{x->})5 (y:= 2 + 3, {x-> 7} (x > 5, {x -> 7})true ? {x->7, y->5} (if x > 5 then y:= 2 + 3 else y:=3 + 4 fi, {x -> 7}) ? {x->7, y->5}Elsa L. Gunter Example 2 + 3 = 5 (2,{x->7})2 (3,{x->7}) 3 7 > 5 = true (2+3, {x->7})5(x,{x->7}) 7 (5,{x->})5 (y:= 2 + 3, {x-> 7}(x > 5, {x -> 7})true {x->7, y->5} (if x > 5 then y:= 2 + 3 else y:=3 + 4 fi, {x -> 7}) ? {x->7, y->5}Elsa L. Gunter Example 2 + 3 = 5 (2,{x->7})2 (3,{x->7}) 3 7 > 5 = true (2+3, {x->7})5(x,{x->7}) 7 (5,{x->})5 (y:= 2 + 3, {x-> 7} (x > 5, {x -> 7})true {x->7, y->5} (if x > 5 then y:= 2 + 3 else y:=3 + 4 fi, {x -> 7}) {x->7, y->5}Elsa L. Gunter Let in Command(E,m) V (C,m[x<-V]) m’(let x = E in C, m) m’’Where m’’(y) = m’(y) for y x and m’’(x) = m(x) if m(x) is defined,and m’’(x) is undefined otherwiseiElsa L. Gunter Example (x,{x->5}) 5 (3,{x->5}) 3 (x+3,{x->5}) 8(5,{x->17}) 5 (x:=x+3,{x->5}) {x->8} (let x = 5 in (x:=x+3), {x -> 17}) ?Elsa L. Gunter Example (x,{x->5}) 5 (3,{x->5}) 3 (x+3,{x->5}) 8(5,{x->17}) 5 (x:=x+3,{x->5}) {x->8}(let x = 5 in (x:=x+3), {x -> 17}) {x ->
View Full Document
Unlocking...