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.