CSc 520 — Principles of Programming Languages53: Semantics — Denotational SemanticsChristian CollbergDepartment of Computer ScienceUniversity of [email protected] 2005 Christian CollbergApril 25, 20051 Denotational Semantics• Denotational semantics gives the meaning of a program in terms of mathematical objects: integers,booleans, tuples, and functions.• The basic idea is to associate a mathematical object with each phrase of the language:– The phrase denotes the mathematical object.– The object is the denotation of the phrase.• Definitions in Denotational Semantics are compositional:– The denotation of a language construct is defined in the denotations of its sub-phrases.2 Meaning Brackets• We use the emphatic (or Strachey or meaning) brackets to enclose pieces of abstract syntax, as in[[p]] .• If p is a phrase in the language, we define a mapping meaning such thatmeaning [[p]]is a mathematical entity that models the semantics of p.3 Meaning Brackets — Examples• Addition in an imperative language:evaluate [[E1+ E2]] sto = compute(m, plus, n)where m = evaluate [[E1]] ston = evaluate [[E2]] sto1• The expressions 2 ∗ 4, (5 + 3), 008, 8 all denote the same abstract object, 8:meaning [[2 ∗ 4]] = meaning [[(5 + 3)]] =meaning [[008]] = meaning [[8]] = 84 Denotational Specification• A denotational specification consists of five parts:1. Syntactic categores2. Abstract production rules3. Semantic domains4. Semantic functions5. Semantic equations.•Example — A Language of Numerals5 Denotational SpecificationSyntactic Domains:• N : Numeral• D : DigitAbstract Production Rules:Numeral ::= Digit | Numeral DigitDigit ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9Semantic Domains:• Number = {0, 1, 2, 3, 4, . . .}6 Denotational Specification. . .Semantic Functions:value : Numeral → Numberdigit : Digit → Number2Semantic Equations:value [[N D]] = 10 ∗ value [[N]] + digit [[D]]value [[D]] = digit [[D]]digit [[0]] = 0...digit [[9]] = 97 Example• Let’s see how the meaning of the phrase 65 would be derived:value [[65]] = 10 ∗ value [[6]] + digit [[5]]= 10 ∗ digit [[6]] + 5= 10 ∗ 6 + 5= 60 + 5 = 658 Example. . .• And the meaning of the phrase 088:value [[088]] = 10 ∗ value [[00]] + digit [[8]]= 10 ∗ (10 ∗ value [[0]] + digit [[0]]) + 8= 10 ∗ (10 ∗ digit [[0]] + 0) + 8= 10 ∗ (10 ∗ 0 + 0) + 8= 8• Note thatvalue [[088]] = digit [[8]] = value [[8]] = 8The Semantics of Wren9 Imperative Languages• Wren is an imperative language.• Programs consist of commands (statements).• Commands alter a store, a global data structure simulating computer memory.• The program updates the store until the required result is reached.• The most important command is the assignment statement which modifies the store.• Basic program control consists of sequencing, selection, and iteration (;, if, while).310 Abstract Syntactic DomainsThese are the abstract syntactic domains of Wren:P : ProgramC: CommandD: DeclarationT : TypeE: ExpressionO: OperatorN: NumeralI: Identifier11 Abstract Syntax of WrensProgram ::= program identifier is Declaration* begin Command endDeclaration ::= var Identifier : TypeType ::= integer | booleanCommand ::= command | Command ; Command | variable := Expression | skip | read read Identifier|write Expression | while Expression do Command | if Expression then Command | if Expressionthen Command else CommandExpression ::= Numeral | Identifier | true | false | | Expression Operator Expression | not ( Expression) | - ( Expression )Operator ::= <= | < | = | > | >= | <> | + | | * | / | and | or12 Semantic Domains of Wren• SV (storable values) represents the values that may be placed in the store.• EV (expressible or first-class values) represents the values that expressions can produce.Integer = {. . . − 2, −1, 0, 1, 2, . . .}Boolean = {true, false}EV = Integer + BooleanSV = Integer + BooleanStore = Identifier → (SV + undefined )413 Semantic Functions of Wren• The value of an expression depends on the values of variables in the store:evaluate : Expression → (Store → EV)• Commands (statements) can modify the store:execute : Command → (Store → Store)• The meaning of a program is its resulting store:meaning : Program → Store• The meaning of a number is handled elsewhere:value : Numeral → EVSemantic Equations14 Commands• The semantics of sequenced commands:execute [[C1; C2]] = execute [[C2]] ◦ execute [[C1]]This could also be written asexecute [[C1; C2]] = execute [[C2]] (execute [[C1]] sto)• skip does not affect the store:execute [[skip]] sto = sto• The assignment statement evaluates the right-hand-side and produces an updated store:execute [[I:= E]] sto = updateSto(sto, I, (evaluate [[E]] sto))15 Commands. . .• Conditionals:execute [[if E then C]] sto = if p thenexecute [[C]] stoelse stowhere p = evaluate [[E]] stoexecute [[if E then C1else C2]] sto = if p thenexecute [[C1]] stoelse execute [[C2]] stowhere p = evaluate [[E]] sto516 Commands. . .• Loops:execute [[while E do C]] sto = loopwhere loop sto = if p thenloop(execute [[C]] sto)else stowhere p = evaluate [[E]] sto• Here we have factored out the looping behavior into a special recursive function loop.17 Expressionsevaluate [[I]] sto = if v = Undefined then error else vwhere v = applySto(sto, I)evaluate [[N]] sto = value [[N]]evaluate [[true]] sto = trueevaluate [[false]] sto = falseevaluate [[E1+ E2]] sto = compute(m, plus, n)where m = evaluate [[E1]] ston = evaluate [[E2]] sto18 Expressions. . .evaluate [[E1/E2]] sto = if n = 0 then errorelse compute(m, div, n)where m = evaluate [[E1]] ston = evaluate [[E2]] stoevaluate [[E1< E2]] sto = if n < m then true else falsewhere m = evaluate [[E1]] ston = evaluate [[E2]] stoevaluate [[E1andE2]] sto = if p then q else falsewhere p = evaluate [[E1]] stoq = evaluate [[E2]] stoA Haskell Prototype619 Abstract Syntaxtype Num = Rationaldata SV = IVal Num | BVal Bool | Undefinedtype Identifier = Stringdata Operator = Add | Sub | Mul | Minus | Div | Not |Or | And | Lt | Gt | Eq | Ne | Le | Gedata Expression = Id String |LitInt Num |TrueVal |FalseVal |Unary Operator Expression |Binary Expression Operator Expression20 Abstract Syntax. . .data Program = Prog [Declaration] Commanddata Declaration = Var [Identifier] Typedata Type = IntType | BoolTypedata Command = Skip |Assign String Expression |Read String |Write Expression |IfThen Expression Command |IfThenElse Expression Command
View Full Document
Unlocking...