Semantics of Formulae

IV.5 Semantics of Formulae

Semantics of formulae [Slide 122]

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

M⟦true⟧(σ₀)	=	tt
M⟦h(e₁,…,e_n)⟧(σ₀) = tt	iﬀ	h(E⟦e₁⟧(σ₀),…,E⟦e_n⟧(σ₀))
M⟦¬f⟧(σ₀) = tt	iﬀ	not (M⟦f⟧(σ₀) = tt)
M⟦f₁ ∧ f₂⟧(σ₀) = tt	iﬀ	(M⟦f₁⟧(σ₀) = tt) and
		(M⟦f₂⟧(σ₀) = tt)

Example 33.

(M⟦¬(Account < 0)⟧(σ₀) = tt)	iﬀ
not (M⟦Account < 0⟧(σ₀) = tt)	iﬀ
not (E⟦Account⟧(σ₀) <E⟦0⟧(σ₀))	iﬀ
not (σ₀(Account) < 0)

Example [Slide 123]

Example 34.

(M⟦Account = 50 ∧In ≥ 0⟧(σ₀) = tt)	iﬀ
(M⟦Account = 50⟧(σ₀) = tt) and (M⟦In ≥ 0⟧(σ₀) = tt)	iﬀ
(E⟦Account⟧(σ₀) =E⟦50⟧(σ₀)) and (E⟦In⟧(σ₀) ≥E⟦0⟧(σ₀))	iﬀ
σ₀(Account) =50 and σ₀(In) ≥0

Semantics of formulae [Slide 124]

Let σ₀ ∼_v σ′₀ denote that the states σ₀ and σ′₀ are identical with the possible exception of the mapping for the variable v.

Example 35.

Let σ₀ and σ′₀ be states.

Let σ₀(Cash) = 0 and σ₀(In) = 2
Let σ′₀(Cash) = 0 and σ′₀(In) = 3

Then σ₀ ∼_In σ′₀.

Semantics of formulae [Slide 125]

The semantics of ∀V f is deﬁned in terms of σ₀ ∼_V σ′₀

M⟦∀V

f⟧(σ₀) = tt

iﬀ

(for all σ′₀ s.t. σ₀ ∼_V σ′₀,M⟦f⟧(σ′₀) = tt)

Example 36.

M⟦∀In In ≥ 0⟧(σ₀) = tt	iﬀ
(for all σ′₀ s.t. σ₀ ∼_In σ′₀,M⟦In ≥ 0⟧(σ′₀) = tt)	iﬀ
(for all σ′₀ s.t. σ₀ ∼_In σ′₀,σ′₀(In) ≥0)

2023-09-12

Contact | Home | ITL home | Course | Proofs | Algebra | FL

© 1996-2023