Let M⟦…⟧(…) be the “meaning” function from Formulae × Σ+ to Bool (set of Boolean values, {tt,ff}) and let σ = σ0σ1… be an interval then
M⟦true⟧(σ) |
= |
tt |
M⟦h(e1,…,en)⟧(σ) = tt |
iff |
h(E⟦e1⟧(σ),…,E⟦en⟧(σ)) |
M⟦¬f⟧(σ) = tt |
iff |
not (M⟦f⟧(σ) = tt) |
M⟦f1 ∧ f2⟧(σ) = tt | iff | (M⟦f1⟧(σ) = tt) and |
(M⟦f2⟧(σ) = tt) |
||
M⟦skip⟧(σ) = tt |
iff |
|σ| = 1 |
(M⟦¬(Account < 0)⟧(σ) = tt) |
iff |
not (M⟦Account < 0⟧(σ) = tt) | iff |
not (E⟦Account⟧(σ) <E⟦0⟧(σ)) | iff |
not (σ0(Account) < 0) |
(M⟦Account = 50 ∧In ≥ 0⟧(σ) = tt) |
iff |
(M⟦Account = 50⟧(σ) = tt) and (M⟦In ≥ 0⟧(σ) = tt) | iff |
(E⟦Account⟧(σ) =E⟦50⟧(σ)) and (E⟦In⟧(σ) ≥E⟦0⟧(σ)) | iff |
σ0(Account) =50 and σ0(In) ≥0 |
Let σ ∼V σ′ denote that the intervals σ and σ′ are identical with the possible exception of the mapping for the variable V .
Let σ and σ′ be intervals.
Let σ0(Cash) = 0 and σ0(In) = 2.
Let σ1(Cash) = 1 and σ1(In) = 4.
Let σ2(Cash) = 1 and σ2(In) = 3.
Let σ′0(Cash) = 0 and σ′0(In) = 3.
Let σ′1(Cash) = 1 and σ′0(In) = 2.
Let σ′2(Cash) = 1 and σ′2(In) = 3.
Then σ ∼In σ′.
The semantics of ∀V f is defined in terms of σ ∼V σ′
M⟦∀V f⟧(σ) = tt | iff | (for all σ′s.t. σ ∼V σ′,M⟦f⟧(σ′) = tt) |
M⟦∀In In ≥ 0⟧(σ) = tt |
iff |
(for all σ′s.t. σ ∼In σ′,M⟦In ≥ 0⟧(σ) = tt) | iff |
(for all σ′s.t. σ ∼In σ′,σ′0(In) ≥0) |
The semantics of ‘chop’ is as follows M⟦f1 ; f2⟧(σ) = tt iff
(exists k, s.t. M⟦f1⟧(σ0…σk) = tt and M⟦f2⟧(σk…σ|σ|) = tt) |
||||||||||||||||
|
Interval σ is a fusion of two intervals σ0…σk (satisfies f1) and σk…σ|σ| (satisfies f2). State σk is shared by both.
The semantics of ‘chopstar’ is as follows M⟦f∗⟧(σ) = tt iff
(exist l0,…,ln s.t. l0 = 0 and ln = |σ|and |
||||||||||||||||||||||||||||||||||
for all 0 ≤ i < n,li ≤ li+1 and M⟦f⟧(σli…σli+1) = tt) |
||||||||||||||||||||||||||||||||||
|
Finite interval σ is the fusion of a finite number of finite sub-intervals each satisfying f.