DOC PREVIEW
UA CSC 520 - Semantics

This preview shows page 1-2-3-4-5 out of 15 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 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 15 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 15 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 15 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 15 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Operational SemanticsOperational Semanticsldots Operational Semantics --- $lambda $-calculusStructural Operational SemanticsInference RulesInference RulesInference Rulesldots Inference Rules --- ExamplesAbstract Syntax of WrenAbstract SyntaxSyntactic CategoriesAbstract Syntax --- IntegersAbstract Syntax --- Integersldots Abstract Syntax --- BooleansAbstract Syntax --- CommandsAbstract Syntax --- Commandsldots Abstract Syntax --- ExampleAbstract Syntax --- Exampleldots Semantics of Wren ExpressionsSemantics of Wren ExpressionsStore Abstract Data TypeStore Abstract Data Typeldots ConfigurationsInference SystemInference Rules for ExpressionsInference Rules for Expressionsldots Inference Rules for Expressionsldots Inference Rules for Expressionsldots Inference Rules for Expressionsldots Inference Rules for Expressionsldots Expression ExampleExpression Exampleldots Semantics of Wren CommandsConfigurationsConfigurationsldots Configurationsldots Command Inference Rules --- AssignCommand Inference Rules --- AssignCommand Inference Rules --- $IF $Command Inference Rules --- $WHILE $Command Inference Rules --- SequencingCommand Inference Rules --- $READ $Command Inference Rules --- $WRITE $An ExampleInput ProgramTransitionsTransitionsldots A Haskel ImplementationAbstract Syntax for Integer ExpressionsConfiguration for ExpressionsBasic ComputationTransition FunctionTop-level Evaluation FunctionTestingThe StoreThe Storeldots Readings and ReferencesAcknowledgments520—Spring 2005—52CSc 520Principles of ProgrammingLanguages52: Semantics — Operational SemanticsChristian [email protected] of Computer ScienceUniversity of ArizonaCopyrightc 2005 Christian Collberg[1]520—Spring 2005—52Operational SemanticsIn this lecture we will describe a method for the formalspecification of programming languages, known asstructural operational semantics.Operation semantics describes how a computation isperformed.We’ve already seen some operational semanticmethods:1. A metacircular interpreter for Scheme,2. Theβ-reduction rule with the normal order reductionstrategy forλ-calculus.[2]520—Spring 2005—52Operational Semantics...An operational semantics operates on a sequence ofstates.We start with an initial state.The program maps the initial state into a new state, andso on, until afinal state is reached, the result of theprogram.[3]520—Spring 2005—52Operational Semantics — λ-calculusA configuration consists of the lambda expressionthat’s left to reduce.The transition function applies β and δ-reductionsaccording to our evaluation strategy.The evaluation terminates when a configuration is innormal form.[4]520—Spring 2005—52Structural Operational SemanticsOperational semantics specifies the semantics of alanguage in terms of how it would be executed on anabstract machine.In Structural Operational Semantics (SOS), definitionsare given byinference rules.SOS turns the abstract machine into a system of logicalinferences.[5]520—Spring 2005—52Inference Rules[6]520—Spring 2005—52Inference RulesInference rules:premise1premise1· · · premisenconclusionThe conclusion follows from the premises.Sometimes we add a condition under which the rule isapplicable:premise1premise1· · · premisenconclusionCondition[7]520—Spring 2005—52Inference Rules...Sometimes there are no premises (this is called anaxiom:conclusionin which case we omit the line:conclusion[8]520—Spring 2005—52Inference Rules — ExamplesExample from Natural Deduction (logical properties ofconjunction (and)):p ∧ qpp ∧ qqp qp ∧ qExample from Natural Deduction (introduction ofuniversal quantifier):P (a)∀xP (x)a does not occur in P(x) or in any as-sumption on which P(a) depends[9]520—Spring 2005—52Abstract Syntax of Wren[10]520—Spring 2005—52Abstract SyntaxThe operational semantics operates on a abstractsyntax of the language.The abstract syntax ignores the surface syntax and onlyspecifies the “essential” parts of each languageconstruct.We can use any convenient way to define the abstractsyntax, EBNF, for example.We use inference rules to specify the abstract syntax.The next slide gives the types of objects that we use toconstruct the abstract syntax from.[11]520—Spring 2005—52Syntactic Categoriesn ∈ Num = Set of numeralsb ∈ {true, false} = Set of Boolean valuesid ∈ Id = Set of integer identifiersbid ∈ Bid = Set of Boolean identifiersiop ∈ Iop = {+, −, ∗, /}rop ∈ Rop = {<, ≤, =, ≥, >, <>}bop ∈ Bop = {and, or}ie ∈ Iexp =Set of integer expressionsbe ∈ Bexp = Set of Boolean expressionsc ∈ Cmd = Set of commands[12]520—Spring 2005—52Abstract Syntax — IntegersObjects from Num may serve as integer expressions:n : iexpn ∈ NumNote that this rule is an abbreviated form ofn : iexpn ∈ NumInteger identifiers may serve as integer expressions:id : iexpid ∈ Id[13]520—Spring 2005—52Abstract Syntax — Integers...Integer unary/binary/relational expressions:ie1: iexp ie2: iexpie1iop ie2: iexpiop ∈ Iopie1: iexp ie2: iexpie1rop ie2: bexprop ∈ Ropie : iexp− ie : iexpRemember thatiop ∈ Iop = {+, −, ∗, /}rop ∈ Rop = {<, ≤, =, ≥, >, <>}ie ∈ Iexp =Set of integer expressions[14]520—Spring 2005—52Abstract Syntax — BooleansObjects from Num may serve as boolean expressions:b : bexpb ∈ {true, false}Boolean identifiers may serve as boolean expressions:bid : bexpbid ∈ BidBoolean binary expressions:be1: bexp be2: bexpbe1bop be2: bexpbop ∈ Bopbe : bexpnot be : bexp[15]520—Spring 2005—52Abstract Syntax — Commandsskip : cmdie : iexpid := ie : cmdid ∈ Idbe : bexpbid := be : cmdbid ∈ Bidread id : cmdid ∈ Idie : iexpwrite ie : cmd[16]520—Spring 2005—52Abstract Syntax — Commands...be : bexp c : cmdif be then c : cmdbe : bexp c1: cmd c2: cmdif be then c1else c2: cmdc1: cmd c2: cmdc1; c2: cmdbe : bexp c : cmdwhile be do c : cmd[17]520—Spring 2005—52Abstract Syntax — ExampleWe can show that the following is a valid Wrencommand by derivingx:= 5 ; while not(x = 0) do x:= x − 1 ; write x : cmdx : iexp 0 : iexpx = 0 : bexpnot(x = 0) : bexpx : iexp 1 : iexpx − 1 : iexpx:= x − 1 : cmdwhile not(x = 0) do x:= x − 1 : cmdThe next slide shows the complete derivation.[18]520—Spring 2005—52Abstract Syntax — Example...5 : iexpx:= 5 : cmdx : iexp 0 : iexpx = 0 : bexpnot(x = 0) : bexpx : iexp 1 : iexpx − 1 : iexpx:= x − 1 : cmdwhile not(x = 0) do x:= x − 1 : cmdx : iexpwrite x : cmdwhile not(x = 0) do x:= x −


View Full Document

UA CSC 520 - Semantics

Documents in this Course
Handout

Handout

13 pages

Haskell

Haskell

15 pages

Recursion

Recursion

18 pages

Semantics

Semantics

12 pages

Scheme

Scheme

32 pages

Syllabus

Syllabus

40 pages

Haskell

Haskell

17 pages

Scheme

Scheme

27 pages

Scheme

Scheme

9 pages

TypeS

TypeS

13 pages

Scheme

Scheme

27 pages

Syllabus

Syllabus

10 pages

Types

Types

16 pages

FORTRAN

FORTRAN

10 pages

Load more
Download 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 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 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?