Denotational Semantics (Denotational Semantics)Formal SemanticsUtility of Formal SemanticsFormal Semantics (continued)UsesAxiomatic SemanticsSlide 7Using Axiomatic SemanticsDenotational SemanticsCandidates f’sScott’s TheoryDefining MomentOn Defining a Language's Denotational SemanticsTermsMore TermsEven More TermsA Small Imperative LanguageA Small Imperative Language (cont)Slide 19Semantic DomainSemantic Domain (cont)(Denotational Semantics)Formal SemanticsWhat does y:= f(x) + x mean?–y is assigned the value of f(x) + x–y becomes a pointer to the result of f(x) + x–f(x) may or may not have side effects–statement is undefined if types aren't equivalent–statement is undefined if types aren't compatible–etc•Need formal semantics to make meanings of programs unambiguous.Utility of Formal Semantics•Handy for:–language design–proofs of correctness–language implementation–reasoning about programs–providing a clear specification of behaviorFormal Semantics (continued)Tennent: " ... a precise specification of the meanings of programs for use by programmers, language designers and implementers, and in the theoretical investigations of language properties.”•Three major approaches:1) Denotational: define functions that map syntactic structures into mathematical objects (e.g. numbers, truth values & functions) (Algebraic) - considered a component of denotational 2) Operational: formal virtual machine description (VDL, H-Graphs) 3) Axiomatic: development of axioms defining meanings of classic statement types. (Dijkstra, Hoare)Uses•Denotational: Ashcroft and Wadge argue best use is language design. (as opposed to retrofit, as attempted with Ada). Used some for formal verification.•Operational: Best for implementation description.•Axiomatic: Most often used for formal verification.Axiomatic SemanticsAxioms:null: {P} skip {P}assignment: {PE} x:= E {P} where PE is the assertion formedby replacing every occurrence of x in P by E.alternation: {P ^ B} S1 {Q}, {P ^ B) S2 {Q}{P} if B then S1 else S2 {Q}iteration: {P ^ B } S {P}{P} while B do S {P ^ B}composition: {P1} S1 {P2},{P2} S2 {P3},…,{Pn} Sn {Pn+1}{P1} begin S1, S2, …, Sn end {Pn+1}x xa: antecedentc: consequentrules of inferenceconsequence: {P1} S {Q1}, P P1, Q1 Q{P} S {Q}await: {P ^ B} S {Q}{P} await B then S {Q}cobegin: {P1} S1 {Q1},…, {Pn} Sn {Qn} are interference free {P1 ^ … ^ Pn} cobegin S1 //…// Sn coend {Q1 ^…^ Qn}Axiomatic SemanticsMore axioms:Uses: Dijkstra’s weakest preconditionsTemporal logicUsing Axiomatic SemanticsProve noninterference in the following: {x=0 and y = 0} S: cobegin s1: await true then y:= y + 1// s2: await true then x:= x + 2// s3: await y>0 then x:= x + y coend {x=3 and y=1}Denotational Semantics•Assigning denotations to language constructs•Utilizes domains and functions over domains–domains are sets with properties that allow us to deal with questions regarding•recursive definitions of functions (over domains)•recursive definitions of domains e.g. consider (recursive function over domain) f: Num  Num -- f: maps numbers into numbersMathematicalrecursionCandidates f’s• Two candidate "defining" functions for f: (i) fx = (fx) + 1 (ii) fx = fx•Assuming Num = {0,1,2,....}, there is no f for (i) and every f satisfies (ii).•In contrast: (iii) fx = (x=0)  1, x * f(x-1) uniquely defines f as factorialScott’s Theory•Scott's (1969) theory of domains ensures every definition is good by:–requiring all domains to have an "implicit structure." This requirement guarantees that all equations (e.g. i, ii and iii) have at least one solution.–providing direction, using implicit structure, for choosing an "intended" solution from the solutions guaranteed by (a).•based on lattices and fixed point theory.•e.g. Num consists of 0, 1, 2, ... and undefined - Num is called a lifted domainDefining Moment•Thus, (i) and (ii) define f to be undefined and (iii) defines f as fx = x! if x=0, 1, 2, ... and f undefined = undefined•Using  as a value is an alternative to using partial functions.• With , all elements in domain have a value.– e.g. f undefined = undefined•Scott's theory applies as well to recursive definitions of domains.–e.g. lists defined in terms of listsOn Defining a Language's Denotational SemanticsThree components:•Abstract syntax (syntactic domain)–list of syntactic categories–list of syntactic clauses (a mapping onto immediate constituents)•Semantic Domain (Semantic Algebras)–domain equations: provide framework for defining denotations–sets that are used as value spaces in PL semantics•Semantic functions–functions that define denotation of constructs–semantic clausesTerms• x.e: Church's lambda notation (seen before)• x.e : A  B ::= (x.e) =  (x.e)a = [a/x]e for a  ^-"proper element"– x.e is e.g. of a strict operation– non-strict operations allow  to be mapped to proper elements•(let x = e1 in e2) is a syntactic substitute for (x.e2)e1•diverge: statement that goes into an infinite loopMore Terms•x  e1  e2: syntactic form for conditional e.g. C[If B THEN C1 ELSE C2] = s.B[B]s  C[C1]s C[C2]s•Expressions in mini-language assumed to have no side effects.–e.g. no reads in expressions.•[i  n]s is a function updating expression ([i  n]s)(i) = n ([i  n]s)(j) = s(j)  j  i–useful for reflecting effects of updating the ith component of a store: ith component changes; rest stays the same–update's signature: Id x Nat x Store  StoreEven More Terms•Interpretation of: P[C.] = n. let s = (update [A] n newstore) in let s' = C[C]s in (access [Z]s')–input number is associated with identifier [A] in a new store–then program body is evaluated–then answer is extracted from store at [Z](program mapping: Nat  Nat --  is possible because diverge is possible)•Clauses for C are all strict in use of store•E does not modify store; expression evaluation order is not specified–e.g. E[E1]s plus E[E2]s•Same for BooleansA Small Imperative Language•Abstract SyntaxP  ProgramC  CommandE  ExpressionB  Boolean-exprN  NumeralP ::= C.C ::=