Next Prev Up

V.2 Integer variable and intervals

Integer variable [Slide 140]

A

integer variable, value of A in the current state

Example 38.  

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

Temporal variable [Slide 141]

A

the value of A in the next state

Example 39.  

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

Temporal variable [Slide 142]

fin A

the value of A in the last state

Example 40.  

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

Derived Operator [Slide 143]

A gets e

A continually gets e, A gets e ≜(skip ⊃ A ← e)

Example 41.  

A = 0 ∧skip2 ∧ A gets A + 1 :
●
●
●
A = 0
A = 1
A = 2

stable A

A remains stable, stable A ≜ A gets A

Quantification [Slide 144]

∃X f

X acts as local variable in f

Example 42.  

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)

Next Prev Up

2024-08-02
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2024