Programming Languages

G22.2110 Spring 1998

Class #13

Denotational Semantics

Contents

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:

Complete

Consistent

Precise

Unambiguous

Concise

Understandable

Useful

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

terms.

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