Programming Languages andCompilers (CS 421)Elsa L Gunter2112 SC, UIUChttp://www.cs.uiuc.edu/class/fa06/cs421/Based in part on slides by Mattox Beckman, as updatedby Vikram Adve and Gul AghaElsa L. GunterNatural Semantics• Similar to transition semantics except– Transition semantics is relationbetween individual steps ofcomputation– Natural semantics is relation betweencomputation state and final result• Rules look like (C, m) ⇓ m’• Always want Lemma: (C,m) -->* m’ iff (C, m) ⇓ m’Elsa L. GunterPicture• Transition semantics(C1,m1) --> (C2,m2) --> (C3,m3) --> … --> m• Natural Semantics (C1,m1) ⇓ mElsa L. GunterNatural Semantics of AtomicExpressions• Same as Transition• Identifiers: (I,m) ⇓ m(I)• Numerals are values: (N,m) ⇓ N• Booleans: (true,m) ⇓ true (false ,m) ⇓ falseElsa L. GunterBooleans:(B, m) ⇓ false (B, m) ⇓ true (B’, m) ⇓ b(B & B’, m) ⇓ false (B & B’, m) ⇓ b (B, m) ⇓ true (B, m) ⇓ true (B’, m) ⇓ b(B or B’, m) ⇓ false (B or B’, m) ⇓ b(B, m) ⇓ true (B, m) ⇓ false(not B, m) ⇓ false (not B, m) ⇓ trueElsa L. GunterRelations(E, m) ⇓ U (E’, m) ⇓ V U ~ V = b(E ~ E’, m) ⇓ b• By U ~ V = b, we mean does (themeaning of) the relation ~ hold on themeaning of U and V• May be specified by a mathematicalexpression/equation or rules matchingU and VElsa L. GunterArithmetic Expressions(E, m) ⇓ U (E’, m) ⇓ V U op V = N(E op E’, m) --> (E’’ op E’,m)where N is the specified value for U op VElsa L. GunterCommands(skip, m) ⇓ m(E,m) ⇓ V(I::=E,m) ⇓ m[I <-- V ](C,m) ⇓ m’ (C’,m’) ⇓ m’’(C;C’, m) ⇓ m’’Elsa L. GunterIf 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. GunterWhile 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. GunterExample (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. GunterExample (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. GunterExample (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. GunterExample (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. GunterExample (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}) ⇓ ? {x->7, y->5}Elsa L. GunterExample (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 ⇓ ? .(if x > 5 then y:= 2 + 3 else y:=3 + 4 fi, {x -> 7}) ⇓ ? {x->7, y->5}Elsa L. GunterExample (2,{x->7})⇓2 (3,{x->7}) ⇓3 (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. GunterExample (2,{x->7})⇓? (3,{x->7}) ⇓? (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. GunterExample (2,{x->7})⇓2 (3,{x->7}) ⇓3 (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. GunterExample (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}) ⇓ ? {x->7, y->5}Elsa L. GunterExample (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}) ⇓? {x->7, y->5}Elsa L. GunterExample (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}) ⇓ {x->7, y->5}Elsa L. GunterLet 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 andm’’(x) = m(x) if m(x) is defined,and m’’(x) is undefined otherwiseiElsa L. GunterExample (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. GunterExample (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 -> 17}Elsa L. GunterComment• Simple Imperative
View Full Document
Unlocking...