Programming Languages andCompilers (CS 421)Elsa L Gunter2112 SC, UIUChttp://www.cs.uiuc.edu/class/sp07/cs421/Based in part on slides by Mattox Beckman, as updatedby Vikram Adve and Gul AghaElsa L. GunterSemantics• Expresses the meaning of syntax• Static semantics– Meaning based only on the form ofthe expression without executing it– Usually restricted to type checking /type inferenceElsa L. GunterDynamic semantics• Method of describing meaning ofexecuting a program• Several different types:–Operational Semantics–Axiomatic Semantics–Denotational SemanticsElsa L. GunterDynamic Semantics• Different languages bettersuited to different types ofsemantics• Different types of semanticsserve different purposesElsa L. GunterOperational Semantics• Start with a simple notion of machine• Describe how to execute (implement)programs of language on virtualmachine, by describing how to executeeach program statement (ie, followingthe structure of the program)• Meaning of program is how itsexecution changes the state of themachine• Useful as basis for implementationsElsa L. GunterAxiomatic Semantics• Also called Floyd-Hoare Logic• Based on formal logic (first orderpredicate calculus)• Axiomatic Semantics is a logicalsystem built from axioms andinference rules• Mainly suited to simple imperativeprogramming languagesElsa L. GunterAxiomatic Semantics• Used to formally prove a property(post-condition) of the state (the valuesof the program variables) after theexecution of program, assuminganother property (pre-condition) of thestate before execution• Written :{Precondition} Program {Postcondition}• Source of idea of loop invariantElsa L. GunterDenotational Semantics• Construct a function M assigning amathematical meaning to each programconstruct• Lambda calculus often used as the range of themeaning function• Meaning function is compositional: meaning ofconstruct built from meaning of parts• Useful for proving properties of programsElsa L. GunterDenotational Semantics• Construct a function M assigning amathematical meaning to each programconstruct• Meaning function is compositional:meaning of construct built from meaningof parts• Useful for proving properties of programsElsa L. GunterNatural Semantics• Aka Structural Operational Semantics,aka “Big Step Semantics”• Provide value for a program by rulesand derivations, similar to typederivations• Rule conclusions look like(C, m) ⇓ m’(E, m) ⇓ vElsa L. GunterSimple ImperativeProgramming Language• I ∈ Identifiers• N ∈ Numerals• B ::= true | false | B & B | B or B | not B| E < E | E = E• E::= N | I | E + E | E * E | E - E | - E• C::= skip | C;C | I ::= E| if B then C else C fi | while B do C odElsa L. GunterNatural Semantics of AtomicExpressions• 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) ⇓ 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. 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) ⇓ Nwhere N is the specified value for U op VElsa L. GunterCommandsSkip: (skip, m) ⇓ mAssignment: (E,m) ⇓ V (I::=E,m) ⇓ m[I <-- V ]Sequencing: (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->7})⇓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->7})⇓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->7})⇓? (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 7 > 5 = true (2+3, {x->7})⇓5(x,{x->7})⇓7 (5,{x->7})⇓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 7 > 5 = true (2+3, {x->7})⇓5(x,{x->7})⇓7 (5,{x->7})⇓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 7 > 5 = true (2+3, {x->7})⇓5(x,{x->7})⇓7 (5,{x->7})⇓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 7 > 5 = true (2+3, {x->7})⇓?(x,{x->7})⇓7 (5,{x->7})⇓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,
View Full Document
Unlocking...