HW 6

COSC 4780

1 Semantics

The semantics for the core language are given by the following equations.

For Command :

[[L:=E : comm ]](s) = update([[L : intloc ]], [[ E : intexp ]](s), s)

[[ C1 ; C2 : comm ]](s) = [[ C2 : comm ]]([[ C1 : comm ]](s))

[[ if E then C1 else C2 fi : comm ]](s) = if([[ E : boolexp ]](s), [[ C1 : comm ]](s), [[ C2 : comm ]](s))

[[ while E do C od : comm ]](s) = w(s)

where w(s) = if([[ E : boolexp ]](s), w([[ C : comm ]](s)), s)

[[ skip : comm ]](s) = s

For Expression :

[[ k : intexp ]](s) = k

[[ @L : intexp ]](s) = lookup([[L : intloc ]], s)

[[ E1 + E2 : intexp ]](s) = plus([[ E1 : intexp ]](s), [[ E2 : intexp ]](s))

[[ ¬E : boolexp ]](s) = not([[ E : boolexp ]](s))

[[ E1 = E2 : boolexp ]](s) = equalbool([[ E1 : boolexp ]](s), [[ E2 : boolexp ]](s))

[[ E1 = E2 : boolexp ]](s) = equalint([[ E1 : intexp ]](s), [[ E2 : intexp ]](s))

For Location :

[[ loci

: intloc ]] = loci

When P is a syntactic class and τ is a type, the semantic functions are

denoted by Scott brackets as [[ P : τ ]]. These functions have the following

types1

:

(λC. [[ C : comm ]]) : comm → store → store

(λE. [[ E : intexp ]]) : expression → store → int

(λE. [[ E : boolexp ]]) : expression → store → bool

(λL. [[L : inloc ]]) : inloc → inloc

The corresponding OCaml functions and their types are as follows:

meaning of command : command → store → store

1The notation [[ P : τ ]] builds the argument P into the function, we have lambdaabstracted the embedded argument out to show that the meaning function takes the

syntactic phrase P as an argument as well.

1

meaning of intexp : expression → store → int

meaning of boolexp : expression → store → bool

meaning of inloc : inloc → inloc

We can use these semantics as rewrite rules ina left to right fashion to

“evaluate” a program in a store.

So, for example,

[[ loc1:=1; loc2:[email protected] + 1 : comm ]]h0, 1, 0i

hhby the sequencing rule (; )ii

=[[ loc2:[email protected] + 1 : comm ]]([[ loc1:=1 : comm ]]h0, 1, 0i)

hhby the assignment rule.ii

= [[ loc2:[email protected] + 1 : comm ]](update([[ loc1 : intloc ]], [[ 1 : intexp ]]h0, 1, 0i,h0, 1, 0i))

hhby the rule for locations.ii

= [[ loc2:[email protected] + 1 : comm ]](update(loc1, [[ 1 : intexp ]]h0, 1, 0i,h0, 1, 0i))

hhby the rule for integer expressions.ii

= [[ loc2:[email protected] + 1 : comm ]](update(loc1, 1,h0, 1, 0i))

hhby the definition of update.ii

= [[ loc2:[email protected] + 1 : comm ]]h1, 1, 0i

hhby the assignment rule.ii

= update([[ loc2 : loc ]], [[ @loc1 + 1 : intexp ]],h1, 1, 0i,h1, 1, 0i)

hhby the rule for locations.ii

= update(loc2, [[ @loc1 + 1 : intexp ]],h1, 1, 0i,h1, 1, 0i)

hhby the rule for Plus.ii

= update(loc2, Plus([[ @loc1 : intexp ]]h1, 1, 0i, [[ 1 : intexp ]]h1, 1, 0i),h1, 1, 0i)

hhby the rule for dereferencing.ii

= update(loc2, Plus(lookup([[ loc1 : loc ]],h1, 1, 0i), [[ 1 : intexp ]]h1, 1, 0i),h1, 1, 0i)

hhby the definition of lookup.ii

= update(loc2, Plus(1, [[ 1 : intexp ]]h1, 1, 0i),h1, 1, 0i)

hhby the rule for integers.ii

= update(loc2, Plus(1, 1),h1, 1, 0i)

hhby the definition of Plus.ii

= update(loc2, 2,h1, 1, 0i)

hhby the definition of update.ii

h1, 2, 0i)

This is a tedious calculation, which is why it’s nice to have an Ocaml program

that can do it for us.

2

2 Semantics of Side Effecting Expressions

Notice that no expression has an effect on the store, this can be seen by

examining the equations and noticing that the store is not part of the return

value. We say: There are no side-effecting expressions in the language. Lots

of languages have side-effecting expressions; a classic example is the i + +

(+ + i)notation of C. The value of the expression i + + is the value of i

and the expression has the side effect of incrementing the value stored in the

memory location referenced by i. Here’s an idiomatic usage in the C-code

computing the length of a string.

int strlen(cp)

char *cp

{

int count = 0;

while (*cp++) count++;

return count;

}

The variable cp is a pointer to a string. *cp dereferences the pointer to the

string. Recall that strings are terminated by numm (0) so, as soon as the

end of the string is reached, the value of the expression *cp++ is 0, which is

interpreted as false in C and C++ – so the while loop stops.

If we add a side-effecting operation into the expressions in the core language, we need to modify the semantics. We need to modify the return

type of meaning of intexp and meaning of boolexp to account for the

new state – as well as the value of the expression. We’ll add a side effecting

expression of the form L ← E. We extend the expression type in OCaml as

follows:

type expression =

Num of int

| Deref of loc

| Plus of expression * expression

| Not of expression

| Eq of expression * expression

| AssignE of loc * expression

;;

The typing rule for the new expression is as follows:

3

L : intloc E : intexp

L ← E : intexp

To account for side-effects, we must modify the type of the meaning

function to return a pair. In the mathematical presentation, we will write

hx, yi to denote the pair containing x and y. On OCaml this is simply

written (x,y). Here are the types of the new meaning functions.

(λE. [[ E : intexp ]]) : expression → store → (int × store)

(λE. [[ E : boolexp ]]) : expression → store → (bool × store)

In the OCaml code we will have the following.

meaning of intexp : expression → store → (int * store)

meaning of boolexp : expression → store → (bool * store)

The semantics for the new rule is given as:

[[L ← E : intexp ]](s) = let hi, s1i = [[ E : intexp ]](s) in

let s2 = update([[L : intloc ]], i, s1) in

hi, s2i

Thus, the expression E is evaluated (in the current store s) to the value

hi, s1i where i is the value of the expression and s1 is the store that results.

Note that E may have side effects itself. This new store s1 is updated so

that the value i is stored in location L. Note that these expressions could

be nested.

loc2 ← ((loc1 ← (@loc1 + @loc2)) + @loc1)

If we evaluate the left subexpression for the + operator first, this expression

will give a different answer than if we evaluate the right subexpression first.

This means addition is no longer commutative! A similar situation arises

in C++, consider the expression ((i++) + (++i)) and ((++i) + (i++)).

A naive programmer may reason as follows: “Since, a+b = b+a, I should

always be able to swap addends around.”

To add side-effecting expressions, we need to modify all the semantic

equations (even for the non side-effecting expressions) so that they pass the

store around. The rules for addition and Boolean equality need to account

for the order of evaluation of the sub-expressions.

4

[[ k : intexp ]](s) = hk, si

[[ @L : intexp ]](s) = hlookup([[L : intloc ]], s), si

[[ E1 + E2 : intexp ]](s) = lethi1, s1i = [[ E1 : intexp ]](s) in

lethi2, s2i = [[ E2 : intexp ]](s1) in

hi1 + i2, s2i

[[ ¬E : boolexp ]](s) = lethb, s0

i = [[ E : boolexp ]](s)) in

hnot b, s0

i

[[ E1 = E2 : boolexp ]](s) = lethb1, s1i = [[ E1 : boolexp ]](s) in

lethb2, s2i = [[ E2 : boolexp ]](s1) in

hequalbool(b1, b2), s2i

[[ E1 = E2 : boolexp ]](s) = lethi1, s1i = [[ E1 : intexp ]](s) in

lethi2, s2i = [[ E2 : intexp ]](s1) in

hequalint(i1, i2), s2i

For the semantics of commands, we need to update the meaning functions

for those commands that use the meanings of expressions to account for their

own meanings so that they use the pairs properly. We do not have to change

the type of the meaning of command function.

[[L:=E : comm ]](s) = let(i, s1) = [[ E : intexp ]](s) in

update([[L : intloc ]], i, s1)

[[ C1 ; C2 : comm ]](s) = [[ C2 : comm ]]([[ C1 : comm ]](s))

[[ if E then C1 else C2 fi : comm ]](s) = lethb, s1i = [[ E : boolexp ]](s) in

if (b, [[ C1 : comm ]](s1), [[ C2 : comm ]](s1))

[[ while E do C od : comm ]](s) = let w(s) =

lethb, s1i = [[ E : boolexp ]](s) in

if (b, w([[ C : comm ]](s1)), s)

in

w(s)

[[ skip : comm ]](s) = s

Problem 2.1. I have provided code to implement the semantic functions

for the core language. Your assignment is to add the new constructor

to the expression type and to update the functions meaning of intexp,

meaning of boolexp, and meaning of command so that they implement these

new semantics.

5

Sale!