HW 6  COSC 4780 Semantics

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:=@loc1 + 1 : comm ]]h0, 1, 0i
hhby the sequencing rule (; )ii
=[[ loc2:=@loc1 + 1 : comm ]]([[ loc1:=1 : comm ]]h0, 1, 0i)
hhby the assignment rule.ii
= [[ loc2:=@loc1 + 1 : comm ]](update([[ loc1 : intloc ]], [[ 1 : intexp ]]h0, 1, 0i,h0, 1, 0i))
hhby the rule for locations.ii
= [[ loc2:=@loc1 + 1 : comm ]](update(loc1, [[ 1 : intexp ]]h0, 1, 0i,h0, 1, 0i))
hhby the rule for integer expressions.ii
= [[ loc2:=@loc1 + 1 : comm ]](update(loc1, 1,h0, 1, 0i))
hhby the definition of update.ii
= [[ loc2:=@loc1 + 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