ITL
© 1996-2015







23 Semantics of Expressions

Let ⟦...⟧e be the “meaning” (semantic) function from Expressions  × (Σ+ ∪ Σ ω) to V al and let σ = σ0 σ1... be an interval then

|------------------------------------------------------------|
|⟦z⟧eσ             =  z                                       |
|⟦a⟧eσ             =  σ0 (a )and                               |
|                    forall0 < i ≤ |σ|,σi(a) = σ0(a)          |
|⟦A ⟧eσ             =  σ0 (A )                                  |
|⟦g(e1,...,en)⟧eσ  =  g{(⟦e1⟧eσ,...,⟦en⟧eσ)                      |
|⟦  A⟧e           =     σ1(A)               implies |σ | > 0   |
| C   σ              {  choose-any-from (Val)  otherw ise         |
|⟦finA ⟧e          =     σ|σ|(A )             implies σ isfinite  |
|      σ                choose-any-from (Val)  otherw ise         |
--------------------------------------------------------------

Example 16

⟦Account  ⟧eσ = σ0 (Account )
        e
⟦deposit⟧σ = σ0 (deposit) and
forallis.t. 0 < i ≤ |σ |,σi(deposit) = σ0(deposit)
⟦Account  + deposit⟧eσ =
⟦Account  ⟧eσ+ ⟦deposit⟧eσ =
σ0(Account )+σ0 (deposit)
andforallis.t. 0 < i ≤ |σ|,σi(deposit) = σ0(deposit)

_____________________________________________________________________