### 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

 M⟦true⟧(σ0) = tt M⟦P⟧(σ0) = σ0(P) M⟦h(e1,…,en)⟧(σ0) = tt iﬀ h(E⟦e1⟧(σ0),…,E⟦en⟧(σ0)) M⟦¬f⟧(σ0) = tt iﬀ not (M⟦f⟧(σ0) = tt) M⟦f1 ∧ f2⟧(σ0) = tt iﬀ (M⟦f1⟧(σ0) = tt) and (M⟦f2⟧(σ0) = tt)

Example 33.

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

#### Example [Slide 121]

Example 34.

 (M⟦Account = 50 ∧ In ≥ 0⟧(σ0) = tt) iﬀ (M⟦Account = 50⟧(σ0) = tt) and (M⟦In ≥ 0⟧(σ0) = tt) iﬀ (E⟦Account⟧(σ0) =E⟦50⟧(σ0)) and (E⟦In⟧(σ0) ≥E⟦0⟧(σ0)) iﬀ σ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 deﬁned in terms of σ0 v σ0

 M⟦∀v f⟧(σ0) = tt iﬀ (for all σ′0 s.t. σ0 ∼v σ′0,M⟦f⟧(σ′0) = tt)

Example 36.

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

 2018-03-10 Contact | Home | ITL home | Course | Proofs | Algebra | FL