Let E⟦…⟧(…) be the “meaning” (semantic) function from Expressions × Σ+ to Val and let σ = σ0σ1… be an interval then
E⟦z⟧(σ) |
= |
z |
||||
E⟦A⟧(σ) |
= |
σ0(A) |
||||
E⟦ig(ie1,…,ien)⟧(σ) |
= |
g(E⟦ie1⟧(σ),…,E⟦ien⟧(σ)) |
||||
E⟦ A⟧(σ) |
= |
|
||||
E⟦fin A⟧(σ) |
= |
σ|σ|(A) |
||||
E⟦b⟧(σ) | = | b |
||||
E⟦Q⟧(σ) |
= |
σ0(Q) |
||||
E⟦bg(be1,…,ben)⟧(σ) |
= |
bg(E⟦be1⟧(σ),…,E⟦ben⟧(σ)) |
||||
E⟦ Q⟧(σ) |
= |
|
||||
E⟦fin Q⟧(σ) |
= |
σ|σ|(Q) |
||||
E⟦Account⟧(σ) = σ0(Account) |
E⟦Account −Out⟧(σ) = |
E⟦Account⟧(σ)−E⟦Out⟧(σ) = |
σ0(Account)−σ0(Out) |