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 this lecture, you should◮have a high-level view of several different methods of givingsemantics to programming languages◮be able to read and understand language definitions givenusing transition semanticsMark 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 meaning based solely on the form ofa language construct, or the syntax – not based on execution.These are usually restricted to type checking and inference.◮Dynamic semantics provide meaning based on models ofevaluation for the language. 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 be easier to represent certain languages with certaintypes of semantics◮the types of semantics are complementary – they are good fordifferent purposes, 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 the 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 follow 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 system build from axiomsand inference rules◮mainly suited to simple imperative languages◮used to prove a post-condition from a pre-condition: givensomething holds in the starting state, we can show somethingelse holds in 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 composing the meaningsof its components◮useful for proving properties of programs – used for early typesoundness proofs and in theorem provers (plus elsewhere)Mark Hills CS421 Lecture 15: Transition SemanticsOutlineLanguage SemanticsTransition SemanticsAn Overview of SemanticsVarieties of Language SemanticsAlternative MethodsThere are many other methods which have been devised to givesemantics to languages.◮“Compiler-based” semantics – the meaning is whatever thecompiler says it is◮Abstract Machines – similar to operational, an abstractmachine with instructions, etc is devised and used to givesemantics◮Term Rewriting – semantics are formulated as term rewritingsystems, with evaluation given by the rewriting relation◮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 specified as transitions between configurations,altering the machine state◮Rules of the form: hC , mi → hC′, m′i◮C , C′represents the code yet to be executed◮m, m′represents the state (store, memory, etc), often a finitemap from names to values◮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 Lo c◮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 specify the syntax for IMP as:Aexp a ::= n | X | a0+ a1| a0− a1| a0× a1Bexp b ::= true | false | a0= a1| a0≤ a1| ¬b |
View Full Document