ITL
© 1996-2018







IV.5 Semantics of Formulae

Semantics of formulae [Slide 120]

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

Mtrue(σ0)
=
tt
MP(σ0)
=
σ0(P)
Mh(e1,,en)(σ0) = tt
iff
h(Ee1(σ0),,Een(σ0))
M¬f(σ0) = tt
iff
not (Mf(σ0) = tt)
Mf1 f2(σ0) = tt
iff
(Mf1(σ0) = tt) and
(Mf2(σ0) = tt)

Example 33.  

(M¬(Account < 0)(σ0) = tt)
iff
not (MAccount < 0(σ0) = tt)
iff
not (EAccount(σ0) <E0(σ0))
iff
not (σ0(Account) < 0)

Example [Slide 121]

Example 34.  

(MAccount = 50 In 0(σ0) = tt)
iff
(MAccount = 50(σ0) = tt) and (MIn 0(σ0) = tt)
iff
(EAccount(σ0) =E50(σ0)) and (EIn(σ0) E0(σ0))
iff
σ0(Account) =50 and σ0(In) 0

Semantics of formulae [Slide 122]

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 35.  

Let σ0 and σ0 be states.

  • Let σ0(Cash) = 0 and σ0(In) = 2
  • Let σ0(Cash) = 0 and σ0(In) = 3

Then σ0 In σ0.

Semantics of formulae [Slide 123]

The semantics of v f is defined in terms of σ0 v σ0

Mv f(σ0) = tt
iff
(for all σ0 s.t. σ0 v σ0,Mf(σ0) = tt)

Example 36.  

MIn In 0(σ0) = tt
iff
(for all σ0 s.t. σ0 In σ0,MIn 0(σ0) = tt)
iff
(for all σ0 s.t. σ0 In σ00(In) 0)







2018-02-25
Contact | Home | ITL home | Course | Proofs | Algebra | FL