A
integer variable, value of A in the current state
A = 0 ∧ (skip ; (A = 1 ∧empty))
A = 0 : | ● | … |
A = 0 | ||
skip : |
● |
● |
(A = 1 ∧empty) : |
● |
|
A = 1 |
||
skip ; (A = 1 ∧empty) : |
● |
● |
A = 1 |
||
A = 0 ∧ (skip ; (A = 1 ∧empty)) : |
● |
● |
A = 0 |
A = 1 |
|
A
the value of A in the next state
A = 0 ∧skip ∧ ( A) = 1
A = 0 : | ● | … |
A = 0 | ||
skip ∧ ( A) = 1 : |
● |
● |
A = 1 |
||
A = 0 ∧skip ∧ ( A) = 1 : |
● |
● |
A = 0 |
A = 1 | |
A := e
unit assignment, A := e ≜ ( A) = e
fin A
the value of A in the last state
A = 0 ∧skip2 ∧ (fin A) = 1
A = 0 : | ● | … | |
A = 0 | |||
skip2 ∧ (fin A) = 1 : |
● |
● |
● |
A = 1 |
|||
A = 0 ∧skip2 ∧ (fin A) = 1 : |
● |
● |
● |
A = 0 |
A = 1 | ||
A ← e
temporal assignment, A ← e ≜ (fin A) = e
A gets e
A continually gets e, A gets e ≜(skip ⊃ A ← e)
stable A
A remains stable, stable A ≜ A gets A
∃X f
X acts as local variable in f
A = 0 ∧skip2 ∧ A gets A + 1 : | ● | ● | ● |
|
A = 0 |
A = 1 |
A = 2 |
||
∃A |
A = 0 ∧skip2 ∧ : |
|||
A gets A + 1 ∧ B = fin(A) : |
● |
● |
● |
|
B = 2 |
||||
len(n)
length of an interval, len(n) ≜∃I (I = 0) ∧ (I gets I + 1) ∧ (I ← n)