ITL
© 1996-2015







24 Semantics of Formulae

Let ⟦...⟧ be the “meaning” function from F ormulae  × (Σ+  ∪Σ ω) to Bool (set of Boolean values, {tt,ff} ) and let σ = σ0 σ1... be an interval then

|----------------------------------------------------|
|⟦true⟧σ               =   tt                         |
|⟦q⟧σ                 =   σ0 (q)andforall0 < i ≤ |σ|, |
|                         σi(q) = σ0(q)              |
|⟦Q ⟧σ                 =   σ0 (Q)                     |
|⟦h(e1,...,en)⟧σ = tt  iff  h (⟦e1⟧eσ,...,⟦en⟧eσ)         |
|⟦f ⟧σ =  tt           iff  not(⟦f⟧σ = tt)              |
|⟦f1 ∧ f2⟧σ =  tt       iff  (⟦f1⟧σ = tt)and (⟦f2⟧σ = tt)  |
|⟦skip⟧σ = tt          iff  |σ| = 1                    |
------------------------------------------------------

Example 17

(⟦ (Account  <  0)⟧σ = tt)   iff
not(⟦Account  < 0⟧σ = tt)   iff
not(⟦Account ⟧e< ⟦0⟧e )     iff
not(σ0 (Accountσ )<  σ0)

_____________________________________________________________________

Example 18

(⟦Account  = 50 ∧ Deposit ≥  0⟧σ = tt)            iff
(⟦Account  =e 50⟧σ =e tt) and(⟦Deposite ≥ 0⟧eσ = tt)   iff
(⟦Account ⟧σ= ⟦50⟧σ)and (⟦Deposit ⟧σ≥ ⟦0⟧σ)        iff
σ0(Account )=50 andσ0 (Deposit)≥0

_____________________________________________________________________

Let σ ~v  σ′ denote that the intervals σ and σ′ are identical with the possible exception of the mapping for the variable v .

Example 19 Let σ and σ ′ be intervals.

  • Let σ0(Cash ) = 0 and σ0(Deposit ) = 2 .

    Let σ1(Cash ) = 1 and σ1(Deposit ) = 4 .

    Let σ2(Cash ) = 1 and σ2(Deposit ) = 3 .

  • Let σ′0(Cash ) = 0 and σ′0(Deposit ) = 3 .

    Let σ′(Cash ) = 1
 1 and σ′(Deposit ) = 2
 0 .

    Let  ′
σ2(Cash ) = 1 and  ′
σ2(Deposit ) = 3 .

Then σ ~Deposit σ ′ .

_____________________________________________________________________

The semantics of ∀v o f is defined in terms of σ ~v  σ′

|-------------------------------------------------|
| ⟦∀v o f⟧ = tt iff   (forallσ′ s.t. σ ~v σ ′,⟦f⟧σ′ = tt)
---------------------------------------------------

Example 20

⟦∀Deposit  o Deposit ≥ 0⟧σ = tt                 iff
(forallσ ′ s.t. σ ~Deposit σ ′,⟦Deposit ≥ 0⟧σ = tt) iff
(forallσ ′ s.t. σ ~Deposit σ ′,σ′0(Deposit )≥0 )

_____________________________________________________________________

The semantics of ‘chop’ is as follows ⟦f ; f ⟧ = ttiff
  1   2σ

|---------------------------------------------|
| (exists-k, s.t. ⟦f1⟧σ0...σk-=-ttand-⟦f2⟧σk...σ|σ| = tt)
| | | < —f1 —  > | < —f2 — >   |  |           |
| | σ0          σk           σ|σ| |           |
| | ∙     ⋅⋅⋅    ∙    ⋅⋅⋅     ∙   |           |
| ----------------------------------          |
-----------------------------------------------

Interval σ is a fusion of two intervals σ0 ...σk (satisfies f1  ) and σk ...σ|σ| (satisfies f2  ). State σk is shared by both.

|----------------------------|
| or(σ isinfinite and ⟦f1 ⟧σ = tt)|
||----------------|          |
||  | < — f1 — >  |          |
|| σ0             |          |
|| ∙     ⋅⋅⋅      |          |
|------------------          |
------------------------------

Interval σ is infinite and satisfies f
 1  , so f
 2  is irrelevant.

The semantics of ‘chopstar’ is as follows ⟦f*⟧ = ttiff

ifσ isfinite then

|-------------------------------------------------------------|
|   (existl0,...,ln s.t. l0 = 0and ln = |σ|and                    |
|    forall0 ≤ i < n,li ≤ li+1 and⟦f ⟧σli...σli+1 = tt)              |
| |---------------------------------------------------------| |
| | | < —f — >  | ⋅⋅⋅ | < —f — >   |  ⋅⋅⋅  | <  —f — >  |   | |
| |σ0          σl1   σli         σli+1  σln-1          σ|σ| | |
| --∙----⋅⋅⋅----∙-⋅⋅⋅-∙----⋅⋅⋅-----∙--⋅⋅⋅-∙------⋅⋅⋅----∙---- |
----------------------------------------------------------------

Finite interval σ is the fusion of a finite number of finite sub-intervals each satisfying f .

else

|--------------------------------------------------------|
|  (existl0,...,ln s.t. l0 = 0 and                          |
|   ⟦f ⟧σln...|σ| = ttand                                   |
|    forall0 ≤ i < n,li ≤ li+1 and ⟦f ⟧σl ...σl = tt)          |
||----------------------------------i---i+1------------|  |
||  | < —f — >  | ⋅⋅⋅ | < —f  — >   | ⋅⋅⋅ | < —f  — >  |  |
|| σ0          σl1  σli          σli+1   σln           |  |
|--∙----⋅⋅⋅-----∙-⋅⋅⋅-∙----⋅⋅⋅-----∙--⋅⋅⋅-∙-----⋅⋅⋅-----|  |
----------------------------------------------------------
                                                         |
Infinite interval σ is the fusion of a finite number of sub-intervals each satisfying f . Each sub-interval is finite except the last one which is infinite.

or

|--------------------------------------------|
|  (existan infinite num berofli s.t. l0 = 0 and      |
|    forall0 ≤ i,li ≤ li+1 and⟦f ⟧σ ...σ    = tt)  |
||-----------------------------li--li+1---|   |
||  | < —f — >  | ⋅⋅⋅ | < —f — >   | ⋅⋅⋅ |   |
|| σ0          σl1   σli          σli+1    |   |
||  ∙    ⋅⋅⋅    ∙ ⋅⋅⋅ ∙    ⋅⋅⋅     ∙ ⋅⋅⋅ |   |
|-----------------------------------------   |
---------------------------------------------|
Infinite interval σ is the fusion of an infinite number of finite sub-intervals each satisfying f .