Programming Languages and Compilers (CS 421)SemanticsDynamic semanticsDynamic SemanticsOperational SemanticsAxiomatic SemanticsSlide 7Denotational SemanticsSlide 9Transition SemanticsExpressions and ValuesSimple Imperative Programming LanguageTransitions for ExpressionsBooleans:RelationsArithmetic ExpressionsCommands - in EnglishCommandsIf Then Else Command - in EnglishIf Then Else CommandWhile CommandExample EvaluationSlide 23Slide 24Slide 25Slide 26Slide 27Slide 28Slide 29Transition Semantics EvaluationAdding Local DeclarationsCall-by-value (Eager Evaluation)Call-by-name (Lazy Evaluation)Church-Rosser PropertyDoes It always Hold?Transition Semantics for -CalculusProgramming 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 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 Transition Semantics•Form of operational semantics•Describes how each program construct transforms machine state by transitions•Rules look like(C, m) --> (C’, m’)•C, C’ is code remaining to be executed•m, m’ represent the state/store/memory/environment –Partial mapping from identifiers to values–Sometimes m (or C) not needed•Indicates exactly one step of computationElsa L. Gunter Expressions and Values•Special class of expressions designated as values–Eg 2, 3 are values, but 2+3 is only an expression•Memory only holds values•Transitions stop when C is a value•Value is the final meaning of original expression (in the given state)•C, C’ used for commands; E, E’ for expressions; U,V for valuesElsa 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 Transitions for Expressions•Identifiers: (I,m) --> m(I)•Numerals are values: (N,m) --> N•Notation - Function update:•m[I<--V] = y. if y = I then V else m(y)Elsa L. Gunter Booleans: •Values = {true, false}•Operators: (short-circuit)(false & B, m) --> false (B, m) --> (B’’, m)(true & B, m) --> B (B & B’, m) --> (B’’ & B, m)(true or B, m) --> true (B, m) --> (B’’, m)(false or B, m) --> B (B or B’, m) --> (B’’ or B, m)(not true, m) --> false (B, m) --> (B’, m)(not false, m) --> true (not B, m) --> (not B’, m)Elsa L. Gunter Relations(E, m) --> (E’’,m) (E ~ E’, m) --> (E’’~E’,m)(E, m) --> (E’,m) (V ~ E, m) --> (V~E’,m)(U ~ V, m) --> true or false, depending on whether U ~ V holds or notElsa L. Gunter Arithmetic Expressions(E, m) --> (E’’,m) (E op E’, m) --> (E’’ op E’,m)(E, m) --> (E’,m) (V op E, m) --> (V op E’,m)(U op V, m) -->N where N is the specified value for U op VElsa L. Gunter Commands - in English•skip is done evaluating•When evaluating an assignment, evaluate the expression first•If the expression being assigned is already a value, update the memory with the new value for the identifier•When evaluating a sequence, work on the first command in the sequence first•If the first command evaluates to a new memory (ie completes), evaluate remainder with new memoryElsa L. Gunter Commands(skip, m) --> m(E,m) --> (E’,m)(I::=E,m) --> (I::=E’,m) (I::=V,m) --> m[I <-- V ](C,m) --> (C’’,m’) (C,m) --> m’(C;C’, m) --> (C’’;C’, m’) (C;C’, m) --> (C’, m’)Elsa L. Gunter If Then Else Command - in English•If the boolean guard in an if_then_else is true, then evaluate the first branch•If it is false, evaluate the second branch•If the boolean guard is not a value, then start by evaluating it first.Elsa L. Gunter If Then Else Command(if true then C else C’ fi, m) --> (C, m)(if false then C else C’ fi, m) --> (C’, m)(B,m) --> (B’,m)(if B then C else C’ fi, m) --> (if B’ then C else C’ fi, m)Elsa L. Gunter While Command(while B do C od, m) --> (if B then C;while B do C od else skip fi, m) In English: Expand a While into a test of the boolean guard, with the true case being to do the body and then try the while loop again, and the false case being to stop.Elsa L. Gunter Example Evaluation•First step:(if x > 5 then y:= 2 + 3 else y:=3 + 4 fi, {x -> 7})--> ?Elsa L. Gunter Example Evaluation•First step:(x > 5, {x
View Full Document
Unlocking...