ITL
© 1996-2015







18 Semantics of Formulae

Let ⟦...⟧ be the “meaning” function from Formulae  × Σ to Bool (set of Boolean values, {tt,ff} ) and let σ0  be a state then

|-----------------------------------------------------|
| ⟦true⟧σ0             =   tt                          |
| ⟦q⟧σ0               =   σ0(q)                       |
| ⟦Q⟧σ0               =   σ0(Q )                      |
| ⟦h(e1,...,en)⟧σ0 = ttiff  h (⟦e1⟧eσ0,...,⟦en ⟧eσ0)         |
| ⟦f ⟧σ0 = tt         iff  not(⟦f⟧σ0 = tt)              |
| ⟦f1 ∧ f2⟧σ0 = tt     iff  (⟦f1⟧σ0 = tt)and(⟦f2⟧σ0 = tt) |
-------------------------------------------------------

Example 11

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

_____________________________________________________________________

Example 12

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

_____________________________________________________________________

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

Example 13 Let σ
 0  and σ ′
 0  be states.

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

Then σ  ~       σ′
 0  Deposit 0  .

_____________________________________________________________________

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

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

Example 14

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

_____________________________________________________________________