Homework 2: Denotational Semantics of D

Assigned: Wednesday, March 1, 2006
Due: Monday, March 13, 2006 (flexible)

The Assignment

Consider a simple programming language that contains

• variables
• expressions
• input statements
• output statements
• assignment statements
• conditionals
• sequences of statements

The language will only operate on natural numbers (integers). Let's call this language D, for the grade it deserves. In the following sections, I define the key domains and type equations for the language. Your goal is to define a semantics for that language. For example, the meaning of the sequence

```read(a);
write(a+b);
```

should be a function from the a list of numbers (the input) to a list that contains the sum of the first two numbers on the input list.

Syntactic Domains

```P in Prog
L in SL
S in Stat
E in Exp
V in Val
I in Ide
```

Abstract Syntax

```// Programs
Prog => L
// Lists of statements
SL => S
|  S ; L
// Statements
Stat => I = E
|  if E then L fi
|  if E then L0 else L1 fi
|  write(E)
// Expressions
Exp => E1 + E2
|  E1 * E2
|  E1 - E2
|  E1 / E2
|  (E)
|  V
|  I
```

Semantic Domains

```n in N                   Natural Numbers
env in U = Id -> N    Environments
inp in I = N*            Input (a sequence of numbers)
out in O = N*            Output (a sequence of numbers)
cont in C = U -> I -> O  Continuations
```

Types of the Semantic Functions

```meaningProg : Prog -> I -> O
meaningSL : SL -> C-> U -> I -> O
meaningStat : Stat -> C -> U -> I -> O
meaningExp : Exp -> U -> N
meaningVal : Val -> N
```

Helper Functions

Here are some helper functions that you might find useful.

```// Build a basic environment that assigns 0 to every variable.
basicEnv : U
basicEnv = \x . 0
// A continuation used to clean up at the end of the program.
cleanup : C
cleanup = \env . \inp . nil
// Set the value associated with an identifier in an environment.
setenv : U -> Id -> N -> U
setenv env id num =
\x . (x == id) -> num , (env id)
```

Disclaimer: I usually create these pages on the fly, which means that I rarely proofread them and they may contain bad grammar and incorrect details. It also means that I tend to update them regularly (see the history for more details). Feel free to contact me with any suggestions for changes.

This document was generated by Siteweaver on Wed May 10 09:02:34 2006.
The source to the document was last modified on Wed Apr 12 15:22:13 2006.
This document may be found at `http://www.cs.grinnell.edu/~rebelsky/Courses/CS302/2006S/Homework/hw.02.html`.

You may wish to validate this document's HTML ; ; Check with Bobby

Samuel A. Rebelsky, rebelsky@grinnell.edu