Programming Languages

G22.2110 Spring 1998


Class #13

Denotational Semantics





C13.0. Current Assignments, PL Project #4

C13.1. Formal Semantics

C13.2. Denotational Semantics

C13.3. Language of Decimal Numerals

C13.4. Language of Regular Expressions

C13.5. Language of Propositional Logic

C13.6. Language of Simple Expressions

C13.7. Other Languages


C13.0. Current Assignments, PL Project #4


PL Project Part IV due today.


C13.1. Formal Semantics


Meaning of lanugages should be:









Possible uses of formal semantics:

Standardization of Programming Languages

References for users

Proof of program correctness

Reference for implementors

Automatic implementation

Better understanding of language design


Approaches to formal semantics to programming languages:

Operational semantics

Define an abstract machine with primitive instructions

The semantic description of the PL specifies a translation into this code

Denotational semantics

Give functions that map computer programs to the abstract mathematical values

they denote (numbers, truth values, functions, etc.)

Axiomatic semantics

Define the action of a program construct by the logical properties that hold of the

state of the computer before and after the execution of the construct.

Algebraic semantics

Consider objects of computation to be terms in multi-sorted algebras.

Programs implement functions that can be expressed by equations between


Structured operational semantics or natural semantics

Programs are given meaning by derivation rules that describe the evaluation of

the constructs in the language.


C13.2. Denotational Semantics


Denotational approach associates mathematical denotations to syntactical parts of the languages.


Proceed in four steps:

Give the syntactic categories

Define the (abstract) syntax of the language

Give the value domains

Define functions that map each syntactic object to some semantic value


C13.3. Language of Decimal Numerals


Syntactic categories:


D Î Digits the decimal digits

N Î Num decimal numerals


Syntax of decimal numerals (BNF):


D ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9

N ::= D | ND


Mathematical denotations of decimal numerals come from the set of natural numbers:


Nat = {0, 1, 2 , } natural numbers (only value domain required)


Semantic functions:


D : Digits -> Nat

M : Num -> Nat


Following equations define the two semantic functions inductively:


D[0] = 0

D[1] = 1

D[9] = 9

M[D] = D[D]

M[ND] = 10 x M[N] + M[D]

C13.4. Language of Regular Expressions


Syntactic categories:


A Î Alpha the alphabet

R Î RE regular expressions


Abstract syntax of regular expressions:


R ::= A | Æ | (R + R) | (R . R) | R*


Value domains:

Lang formal languages (set of strings over Alpha)


Semantic functions:


A : Alpha -> Lang

D : RE -> Lang


Definition of semantic functions:


A[A] = {A}

D[A] = A[A]

D[Æ ] = { }

D[(R1 + R2)] = D[R1] È D[R2]

D[(R1 . R2)] = {x . y | x Î D[R1] & y Î D[R2]}

D[R*] = È ( i ) (D[R])i


e.g., alphabet containing symbols a and b, D[(Æ + a)] = D[Æ ] È D[a] = {a}, and D[a . Æ ] = { }.


C13.5. Language of Propositional Logic


Syntactic categories:


P Î Prop propositions

F Î Form formulas


Formulas syntax:


F ::= P | Ø F | F Þ F


Value domains:

Bool = { True, False } boolean values

r Î Assign = P -> Bool assignments (reveals if a proposition is true or not)


Semantic functions:


M : Form -> Assign -> Bool


Definition of M:


M[P]r = r (P)

M[Ø F]r = Ø M[F]r

M[F1 => F2]r = Ø M[F1]r Ú M[F2]r


C13.6. Language of Simple Expressions


Syntactic categories:

I Î Ident identifiers

E Î Exp expressions


Language syntax:


E ::= 0 | 1 | I | (E1 + E2) | (E1 - E2) | let I = E1 in E2 end


Value domains:


Int = { , -2, -1, 0, 1, 2, } integers

r Î Env = Ident -> Int environments


Semantic functions:

e : Exp -> Env -> Int


Function definitions:

e [0]r = 0

e [1]r = 1

e [I]r = r (I)

e [E1 + E2]r = e [E1]r + e [E2]r

e [E1 - E2]r = e [E1]r - e [E2]r


e [let I = E1 in E2 end]r = e [E2](r [I -> e [E1]r ])


f[x -> y] means that the function f is modified so that f(x) = y.


e.g., in ML

fun Update (f, x, y) (x0) = if x0 =x then y else f(x0)


C13.7. Other Languages


Language with Error Values

Language with State

Language with Commands

Language Combining Expressions and Commands

Language with Function Calls

Language with goto