CIS 705a Assignment 2
based on Sections 3.1-3.4 of the "Programming Language Semantics" paper
1.
First, there is an error in Figure 4. The very first line should say,
P: Program -> Nat -> Store_
Oh well! Use the semantics in Figure 4 to prove this inequality:
P[[ z = x + 1. ]]
!=
P[[ y = x; z = y + 1. ]]
(the problem is that the programs compute different final storage vectors)
2. The semantics in Figure 4 for Programs should be improved.
Use this:
P'[[ C. ]] = lam n. check( (lam s. lookup(3, s)),
C[[ C ]]init_env (init_store n) )
That is, a program maps an input number to an output number.
(We are trying to hide how the store is used to compute the output.)
Use the new semantics law to prove this equality:
P'[[ z = x + 1. ]] = P'[[ y = x; z = y + 1. ]]
3. Here is the semantics of some boolean expressions:
B: Boolexpr
B ::= ~ B | B1 v B2 | E1 == E2 | E1 > E2
Say we have this "algebra" for truth values:
Boolean = { tt, ff }
not(tt) = ff, not(ff) = tt
or(b1, b2) = logical disjunction
eq(n, n) = tt,
eq(n1, n2) = ff, when n1 is a different int than n2
gt(n1, n2) = tt, when n1 is greater than n2
= ff, when n1 isn't greater than n2
and we have this semantics of boolean expressions:
B: Boolexpr -> Environment -> Store -> Boolean
B[[ ~ B ]] = lam e. lam s. not(B[[ B ]]e s)
B[[ B1 v B2 ]] = lam e. lam s. or(B[[ B1 ]]e s, B[[ B2 ]]e s)
B[[ E1 == E2 ]] = lam e. lam s. eq(E[[ E1 ]]e s, E[[ E2 ]]e s)
B[[ E1 > E2 ]] = lam e. lam s. gt(E[[ E1 ]]e s, E[[ E2 ]]e s)
Prove this logical property:
For all e: Environment, for all s: Store,
if B[[ x > 0 ]]e s = tt,
then
B[[ x > 1 ]]e (C[[ x = x + 1]]e s) = tt
The proof justifies this Hoare-logic claim:
{ x > 0 } x = x + 1 { x > 1 }
Definition: The Hoare triple, {P} C {Q}, is _sound_ iff
for all e: Environment, s: Store,
if B[[ P ]]e s = tt and C[[ C ]]e s = s' != _|_ ,
then B[[ Q ]]e s' == tt
In words: "If P holds true in the current e,s configuration
and C computes an updated store, s',
then Q holds true in the configuration e,s' "
We can prove that all the rules of Hoare-logic
deduce logical truths. Try this one: Prove the soundness of
{ P } C1 { Q } { Q } C2 { R }
----------------------------------
{ P } C1 ; C2 { R }
4. Strachey intended that the Environment hold "immutable" bindings
for names and that the Store hold "mutable" values.
This matches well Algol and C. It matches Java less well and Python less less well.
Here is a first step to understanding why.
Here is a language like the one in the paper but with
explicit int declarations and storage that can grow.
P : Program I : Iden
B : Block
D : Declaration
C : Command N : Numeral
E : Expression
P ::= B.
B ::= D ; C
D ::= int I | proc I = B | D1; D2
C ::= I = E | C1 ; C2 | call I
E ::= N | E1 + E2 | I
ENVIRONMENT DOMAIN:
// an environment is a function/mapping from Idens to "Denotables".
// You can think of a function as a dictionary, like in python.
Environment = Iden -> Denotable // a dictionary works for this
Denotable = Location + Closure + {error}
Location = { 0, 1, 2, ... } // location numbers for indexing the store
Closure = Store -> Store_ // procedure closure --- it needs the run-time store to compute its output
Operations: (Although the environment is a function, I'll write
the operations on dictionaries.)
initenv = {} // empty dictionary
bind(i, d, e) = {i: d} + e // update dictionary e with i:d
// in Python, it's: (e[i] = d; return e)
find(i, e) = e[i], if (i in e)
= error, if (i not in e)
STORE DOMAIN:
// a store is a function/mapping from Location numbers to Ints.
// You can think of the store as a linear list, indexed by 0,1,2,...
Store = Location -> Int
Locations = {0, 1, 2, ...}
Operations: (Although the store is a function, I'll write the operations on lists.)
initstore = [] // empty store
allocate(s) = (len(s), s + [0]) // "list append"
// return new location number and extended store
fetch(loc, s) = s[loc], if loc >= 0 and loc < len(s)
= error, otherwise
update(loc, i, s) = s[:loc] + [i] + s[loc+1:], if loc >= 0 and loc < len(s)
= error, otherwise
// I wrote this in python!
// You can also write it like this: (s[loc] = i; return s)
// Strachey wrote it as [loc |-> i]s
// They all say to update position loc in list s with i.
check(f, s) = f(s), if s : Store
= error, if s = error
= _|_, if s = _|_
P : Program -> Store -> Store_
P[[B.]] = lam s. B[[ B ]]initenv s
B : Block -> Environment -> Store -> Store_
B[[D ; C ]] = lam e. lam s. let (e', s') = D[[D]]e s
in C[[ C ]]e' s'
D : Declaration -> Environment -> Store -> (Environment x Store)
D[[ int I ]] = lam e. lam s. let (newloc, news) = allocate(s)
in (bind(I, inLoc(newloc), e), news)
D[[ proc I = B end ]] = lam e. lam s. (bind(I, inProc(B[[B]]e), e), s)
D[[ D1 ; D2 ]] = lam e. lam s. let (d', s') = D[[ D1 ]] e s
in D[[ D2 ]]d' s'
C : Command -> Environment -> Store -> Store_
C[[ I = E ]] = lam e. lam s.
case (find(I, e) of
inLoc(loc): update(loc, E[[E]]e s, s)
inProc(p): error
inerror: error
C[[C1 ; C2]] = lam e. lam s. check(C[[C2]]e, C[[C1]]e s)
C[[ call I ]] = lam e. lam s.
case (find(I, e) of
inLoc(loc): error
inProc(p): p(s)
inerror: error
E : Expression -> Environment -> Store -> Int_
E[[ N ]] = lam e. lam s. (int)N
E[[E1 + E2]] = lam e. lam s. plus(E[[E1]]e s, E[[E2]]e s)
// I got lazy here and didn't write down the check that we are adding two ints!
E[[ I ]] = lam e. lam s.
case (find(I, e) of
inLoc(loc): fetch(loc, s)
inProc(p): error
inerror: error
In this language, a declaration binds an iden to a "denotable", which
is either a Loc or a Closure. Since a proc can own its own private
declarations, the env used with a proc's body is special to that proc.
All iden lookups must check whether a loc or a closure
is fetched from the env --- there are the "tags" and "cases".
Try the semantics on this example:
int x;
proc p = int y; y = x end;
proc q = int x; call p end;
call q.
The semantics will show how the iden lookups find the correct denotables.
But the semantics manages the Store badly --- when a proc finishes its work,
the cells in the Store allocated for the local vars remain in the Store!
Repair the semantics to make the Store operate like a stack, as in C.
You will add some operations to the Store domain and alter the semantics of Blocks.
5. What if _all_ names have values that can be mutated?
P : Program C : Command
B : Block
D : Declaration E : Expression
N : Numeral I : Identifier
P ::= B .
B ::= D ; C
D ::= var I | D1; D2
C ::= I = E | C1 ; C2 | call I
E ::= N | E1 + E2 | I | { B }
For example:
var x;
var p;
p = { var y; y = x }; // assign a proc body to p
x = 1;
call p;
x = p;
p = 2.
You can do this in a scripting language.
Define a semantics, as best as you can.