Denotational Semantics Formal Semantics What 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 behavior Formal 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 Semantics a antecedent c consequent Axioms null P skip P assignment PE x E P where PE is the assertion formed by 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 x x composition P1 S1 P2 P2 S2 P3 Pn Sn Pn 1 P1 begin S1 S2 Sn end Pn 1 rules of inference Axiomatic Semantics More axioms consequence P1 S Q1 P P1 Q1 Q P S Q await cobegin P B S Q P await B then S Q P1 S1 Q1 Pn Sn Qn are interference free P1 Pn cobegin S1 Sn coend Q1 Qn Uses Dijkstra s weakest preconditions Temporal logic Using Axiomatic Semantics Prove 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 Mathematical recursion e g consider recursive function over domain f Num Num f maps numbers into numbers Candidates 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 factorial Scott 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 domain Defining 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 lists On Defining a Language s Denotational Semantics Three 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 clauses Terms 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 loop More 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 Store Even 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 Booleans A Small Imperative Language Abstract Syntax P Program C Command E Expression B Boolean expr N Numeral Syntactic categories P C C C1 C2 if B then C if B then C1 else C2 I E diverge E E1 E2 I N B E1 E2 B Syntactic clauses A Small Imperative Language cont Semantic domain Semantic Functions P Program Nat Nat functions clauses P C n let s update A n newstore in let s C C s in access Z s C Command Store Store C C1 C2 s C C2 C C1 s C if B then C s B B s C C s s C if B then C1 else C2 s B B s C C1 s C C2 s C I E s update I E E s s C diverge s A Small Imperative Language cont Semantic Functions cont E Expression Store Nat E E1 E2 s E E1 s plus E E2 s E I s access I s E N s B Boolean expr Store Tr B E1 E2 s E E1 s equals E E2 s B B s not B B s N Numeral Nat omitted note Semantic Domain Truth Values Domain t Tr B Operations true false Tr not Tr Tr Identifiers Domain i Id Identifier Natural numbers Domain n Nat N Operations zero one Nat plus Nat x Nat Nat equals Nat x Nat Tr Zero order function Semantic Domain cont Store Domain s Store Id Nat Operations newstore Store newstore i zero access Id Store Nat access i s s i …