Let M⟦…⟧(…) be the “meaning” function from Formulae × Σ to Bool (set of Boolean values, {tt,ff}) and let σ0 be a state then
M⟦true⟧(σ0) |
= |
tt |
M⟦h(e1,…,en)⟧(σ0) = tt |
iff |
h(E⟦e1⟧(σ0),…,E⟦en⟧(σ0)) |
M⟦¬f⟧(σ0) = tt | iff | not (M⟦f⟧(σ0) = tt) |
M⟦f1 ∧ f2⟧(σ0) = tt |
iff |
(M⟦f1⟧(σ0) = tt) and |
(M⟦f2⟧(σ0) = tt) |
(M⟦¬(Account < 0)⟧(σ0) = tt) |
iff |
not (M⟦Account < 0⟧(σ0) = tt) | iff |
not (E⟦Account⟧(σ0) <E⟦0⟧(σ0)) | iff |
not (σ0(Account) < 0) |
(M⟦Account = 50 ∧In ≥ 0⟧(σ0) = tt) |
iff |
(M⟦Account = 50⟧(σ0) = tt) and (M⟦In ≥ 0⟧(σ0) = tt) |
iff |
(E⟦Account⟧(σ0) =E⟦50⟧(σ0)) and (E⟦In⟧(σ0) ≥E⟦0⟧(σ0)) | iff |
σ0(Account) =50 and σ0(In) ≥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.
Let σ0 and σ′0 be states.
Then σ0 ∼In σ′0.
The semantics of ∀V f is defined in terms of σ0 ∼V σ′0
M⟦∀V f⟧(σ0) = tt | iff | (for all σ′0 s.t. σ0 ∼V σ′0,M⟦f⟧(σ′0) = tt) |
M⟦∀In In ≥ 0⟧(σ0) = tt |
iff |
(for all σ′0 s.t. σ0 ∼In σ′0,M⟦In ≥ 0⟧(σ′0) = tt) | iff |
(for all σ′0 s.t. σ0 ∼In σ′0,σ′0(In) ≥0) |