Design (paper part) for chapter 1, problem 2.2, part a.

AUTHOR: Gary T. Leavens

New/Changed Abstract Syntax:

  We replace the old syntax for locations with:
	L ::= int loc i | bool loc i 

  (We use the same as the concrete syntax)

New/Changed type attributes:

  We need attributes for boolean locations.  Thus the attributes are
  generalized to:

        tau ::= int | bool | comm | tau loc | tau exp

New/Changed Type Rules

  The type rule for the assignment command is changed to:

        L: tau loc,
        E: tau exp         if tau \in {int, bool}
        -------------
        L := E : comm

  The dereference expression rule is changed to:

        L: tau loc
        ----------        if tau \in {int, bool}
        @L: tau exp

Sample proofs:

	                      0: int      1:int
                              ----------  ----------
                              0: int exp, 1: int exp
                              ----------------------
        bool loc 1: bool loc, (0 = 1): bool exp
        ---------------------------------------
        bool loc 1 := (0 = 1) : comm



                              bool loc 1: bool loc
                              ----------------------
        bool loc 1: bool loc, (@bool loc 1): bool exp
        ---------------------------------------
        bool loc 1 := not(@bool loc 1) : comm

Unfortunately, these rules are not sound with the usual
kind of store that contains both integers and booleans.
To achieve soundness one has to incorporate the notion
of a type environment as an assumption into the rules,
so one can say what locations are supposed to store
integers and booleans.  But we'll see that in chapter 2...