DOC PREVIEW
U of I CS 421 - Transition Semantics

This preview shows page 1-2-3 out of 8 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 8 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 8 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 8 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 8 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

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

U of I CS 421 - Transition Semantics

Documents in this Course
Lecture 2

Lecture 2

12 pages

Exams

Exams

20 pages

Lecture

Lecture

32 pages

Lecture

Lecture

21 pages

Lecture

Lecture

15 pages

Lecture

Lecture

4 pages

Lecture

Lecture

68 pages

Lecture

Lecture

68 pages

Lecture

Lecture

84 pages

s

s

32 pages

Parsing

Parsing

52 pages

Lecture 2

Lecture 2

45 pages

Midterm

Midterm

13 pages

LECTURE

LECTURE

10 pages

Lecture

Lecture

5 pages

Lecture

Lecture

39 pages

Load more
Download Transition Semantics
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Transition Semantics and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Transition Semantics 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?