Programming Languages and Compilers (CS 421)SemanticsDynamic semanticsDynamic SemanticsOperational SemanticsAxiomatic SemanticsSlide 7Denotational SemanticsSlide 9Natural SemanticsSimple Imperative Programming LanguageNatural Semantics of Atomic ExpressionsBooleans:RelationsArithmetic ExpressionsCommandsIf Then Else CommandWhile CommandExampleSlide 20Slide 21Slide 22Slide 23Slide 24Slide 25Slide 26Slide 27Slide 28Slide 29Slide 30Let in CommandSlide 32Slide 33CommentInterpretation Versus CompilationInterpreterInterpreterNatural Semantics ExampleSlide 39Programming Languages and Compilers (CS 421)Elsa L Gunter2112 SC, UIUChttp://www.cs.uiuc.edu/class/sp07/cs421/Based in part on slides by Mattox Beckman, as updated by Vikram Adve and Gul AghaElsa L. Gunter Semantics•Expresses the meaning of syntax•Static semantics–Meaning based only on the form of the expression without executing it–Usually restricted to type checking / type inferenceElsa L. Gunter Dynamic semantics•Method of describing meaning of executing a program•Several different types:–Operational Semantics–Axiomatic Semantics–Denotational SemanticsElsa L. Gunter Dynamic Semantics•Different languages better suited to different types of semantics•Different types of semantics serve different purposesElsa L. Gunter Operational Semantics•Start with a simple notion of machine•Describe how to execute (implement) programs of language on virtual machine, by describing how to execute each program statement (ie, following the structure of the program)•Meaning of program is how its execution changes the state of the machine•Useful as basis for implementationsElsa L. Gunter Axiomatic Semantics•Also called Floyd-Hoare Logic•Based on formal logic (first order predicate calculus)•Axiomatic Semantics is a logical system built from axioms and inference rules•Mainly suited to simple imperative programming languagesElsa L. Gunter Axiomatic Semantics•Used to formally prove a property (post-condition) of the state (the values of the program variables) after the execution of program, assuming another property (pre-condition) of the state before execution•Written :{Precondition} Program {Postcondition}•Source of idea of loop invariantElsa L. Gunter Denotational Semantics•Construct a function M assigning a mathematical meaning to each program construct•Lambda calculus often used as the range of the meaning function•Meaning function is compositional: meaning of construct built from meaning of parts•Useful for proving properties of programsElsa L. Gunter Denotational Semantics•Construct a function M assigning a mathematical meaning to each program construct•Meaning function is compositional: meaning of construct built from meaning of parts•Useful for proving properties of programsElsa L. Gunter Natural Semantics•Aka Structural Operational Semantics, aka “Big Step Semantics”•Provide value for a program by rules and derivations, similar to type derivations•Rule conclusions look like (C, m) m’(E, m) vElsa L. Gunter Simple Imperative Programming 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. Gunter Natural Semantics of Atomic Expressions•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 CommandsSkip: (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. 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.
View Full Document
Unlocking...