Valuation Functions

The arities of the different valuation functions are:

$$\begin{array}{l} \mbox{\bf P: } \mbox{\em Store} \mapsto \mbo... ...mbox{\em Store} \mapsto \mbox{\em ExpressibleValue} \end{array}$$

The valuation functions are defined according to the following rules:

• 
  
  $$\begin{array}{ll} \mbox{\bf P}[\mbox{\em Command}] = &\lambda... ...em Command}](s\:\:(\mbox{\em empty\_hierarchy}))\\ \end{array}$$
  
  

• 
  
  $$\begin{array}{lll} \mbox{\bf C}[\mbox{\em Command}_1 ; \mbox{... ... in }\\ & {\bf C}[\mbox{\em Command}_2](s'\:\:h') \end{array}$$
  
  

  
  

  $$\begin{array}{lll} {\bf C}[I := E] = & \lambda s. \lambda h. ... ...row (h, \mbox{\em inErr}(s))\\ &\mbox{\em end}&\\ \end{array}$$
  
  

  For the sake of simplicity I am assuming a C-like interpretation of the if-then-else (i.e, the true is represented by any number different from zero).

  
  

  $$\begin{array}{ll} {\bf C}[\mbox{\em if }E\:\:\mbox{\em then }... ...ightarrow (h,\mbox{\em inErr}(s))\\ \mbox{\em end} \end{array}$$
  
  

  
  

  $$\begin{array}{ll} {\bf C}[I := \mbox{\em new }Cl] = & \lambda... ...mbox{\em update }[I]\:\:s\:\:f)))\\ \mbox{\em end} \end{array}$$
  
  

  
  

  $$\begin{array}{lll} {\bf C}[I_1.I_2 := E]=&\lambda s.\lambda h... ...m otherwise} \rightarrow (h,\mbox{\em inErr}(s))\\ \end{array}$$
  
  

  
  

  $$\begin{array}{ll} {\bf C}[\mbox{\em create\_class } Cl\:\:Cl'... ...class }(h \:\:Cl')\:\:Li)\:\:h),\mbox{\em inOK}(s)) \end{array}$$
  
  

• 
  
  $$\begin{array}{ll} {\bf E}[(E)] = \lambda h.\lambda s. {\bf E}[E](h,s)\\ \end{array}$$
  
  

  
  

  $$\begin{array}{lll} {\bf E}[E_1+E_2] = \lambda h.\lambda s. &\... ...{\em otherwise} \rightarrow \mbox{\em inErrValue}() \end{array}$$
  
  

  
  

  $$\begin{array}{lll} {\bf E}[I_1.I_2] = \lambda h.\lambda s. & ... ...\mbox{\em isNat}(n) \rightarrow \mbox{\em inNat}(n) \end{array}$$