OutlineLanguage SemanticsTransition SemanticsCS421 Lecture 15: Transition Semantics1Mark [email protected] of Illinois at Urbana-ChampaignJuly 13, 20061Based on slides by Mattox Beckman, as updated by Vikram Adve, GulAgha, and Elsa GunterMark Hills CS421 Lecture 15: Transition SemanticsOutlineLanguage SemanticsTransition SemanticsLanguage SemanticsTransition SemanticsMark Hills CS421 Lecture 15: Transition SemanticsOutlineLanguage SemanticsTransition SemanticsObjectivesBy the end of t his lecture, you should◮have a high-level view of several different methods of gi vingsemantics to programming languages◮be able to read and understand language definitions givenusing transition s emanticsMark Hills CS421 Lecture 15: Transition SemanticsOutlineLanguage SemanticsTransition SemanticsAn Overview of SemanticsVarieties of Language SemanticsLanguage SemanticsTime flies like an arrow. Fruit flies like a banana.So far, we have syntax, but we don’t know what any of it means!Language semantics provide a way for us to assign meaning toconstructs in a programming language.Mark Hills CS421 Lecture 15: Transition SemanticsOutlineLanguage SemanticsTransition SemanticsAn Overview of SemanticsVarieties of Language SemanticsDynamic vs. StaticSemantics can be grouped into two general categories: staticsemantics and dynamic semantics.◮Static semantics provide me aning based solely on the form ofa language c onstruct, or the syntax – not based on execution.These are usually res trict ed to type checking and inference.◮Dynamic semantics provide meaning based on mo dels ofevaluation for the l anguage. These tell us what it means toexecute a program, for instance.Mark Hills CS421 Lecture 15: Transition SemanticsOutlineLanguage SemanticsTransition SemanticsAn Overview of SemanticsVarieties of Language SemanticsVarieties of SemanticsThere are many methods of giving semantics to a programminglanguage. Several common methods include:◮Operational Semantics◮Axiomatic Semantics◮Denotational SemanticsNote that:◮it may b e easier to represent certain languages with certaintypes of semantics◮the types of semantics are complementary – they are good fordifferent purpos es, with no method “the best”Mark Hills CS421 Lecture 15: Transition SemanticsOutlineLanguage SemanticsTransition SemanticsAn Overview of SemanticsVarieties of Language SemanticsOperational Semantics◮First, start with a definition of our “machine” which we runprograms on◮The machine state, including t he program, is often called theconfiguration◮Next, describe how to execute programs in a given languageby describing how to execute individual statements and partsof statements – rules foll ow the structure of the program◮A program’s “meaning” is defined by how it changes theconfiguration◮Useful as a basis for implementationsMark Hills CS421 Lecture 15: Transition SemanticsOutlineLanguage SemanticsTransition SemanticsAn Overview of SemanticsVarieties of Language SemanticsAxiomatic SemanticsAxiomatic semantics are also called Floyd-Hoare logic◮based on logic – first-order predicate calculus◮semantics represented as a logical sys tem build from axiomsand inference rules◮mainly suited to simple i mperative languages◮used to prove a p ost -condition from a pre-condition: givensomething holds in the starting state, we can show somethingelse holds i n the end state{Precondition} Program {Postcondition}Mark Hills CS421 Lecture 15: Transition SemanticsOutlineLanguage SemanticsTransition SemanticsAn Overview of SemanticsVarieties of Language SemanticsDenotational SemanticsIn denotational semantics, we want to find the meaning, ordenotation, of phrases in our language.◮we construct a function M assigning a mathematical meaningto each language construct;◮these functions are compositional – we can construct themeaning of a language construct by comp osi ng the meaningsof its c omponents◮useful for proving properties of programs – used for early typesoundness proofs and in t heorem provers (plus elsewhere)Mark Hills CS421 Lecture 15: Transition SemanticsOutlineLanguage SemanticsTransition SemanticsAn Overview of SemanticsVarieties of Language SemanticsAlternative MethodsThere are many other metho ds which have b een devised to givesemantics to l anguages.◮“Compiler-based” semantics – the meaning is whatever thecompiler says it is◮Abstract Machines – similar to operational, an abstractmachine with instructions, etc i s devised and used to givesemantics◮Term Rewriting – semantics are formulated as term rewritingsystems, with evaluation given by the rewriting relati on◮Rewriting Logic – an extension of equational logic thatprovides for concurrencyMark Hills CS421 Lecture 15: Transition SemanticsOutlineLanguage SemanticsTransition SemanticsIntroduction to Transition SemanticsA Sample LanguageConfigurationsSemantic RulesExampleExtending the LanguageTransition SemanticsTransition semantics is a form of operational semantics.◮Configurations include the code and machine state: (C , m)◮Semantics sp ec ified as transitions between configurations,altering the machine state◮Rules of t he form: hC , mi → hC′, m′i◮C , C′represents the co de yet to be executed◮m, m′represents the state (store, memory, etc), often a finitemap from names to v alues◮May not need m – simple calculator languages with onlynumbers and operations don’t, for instanceKey point: each transition indicates exactly one step ofcomputationMark Hills CS421 Lecture 15: Transition SemanticsOutlineLanguage SemanticsTransition SemanticsIntroduction to Transition SemanticsA Sample LanguageConfigurationsSemantic RulesExampleExtending the LanguageIMP – A Simple Imperative LanguageWe can use a simple imperative language, IMP, as a samplelanguage for semantics. This language has the following syntacticcategories:◮numbers N, which are the integers (including negatives)◮truth values T = {true, false}◮locations Loc◮arithmetic expressions Aexp◮boolean expressions Bexp◮commands ComFor shorthand,n, m ∈ N; X , Y ∈ Loc; a ∈ Aexp; b ∈ Bexp; c ∈ Com.Mark Hills CS421 Lecture 15: Transition SemanticsOutlineLanguage SemanticsTransition SemanticsIntroduction to Transition SemanticsA Sample LanguageConfigurationsSemantic RulesExampleExtending the LanguageIMP SyntaxUsing a variant of BNF, we can spec ify the syntax for IMP as:Aexp a ::= n | X | a0+ a1| a0− a1| a0× a1Bexp b ::= true |
View Full Document
Unlocking...