From pictorial semantics to first order ITL
● | ● | ● |
A = 2 | A = 2 | A = 2 |
len(2) ∧ A = 2
len(2) ∧ A = 2 ∧ ( A) = 2 ∧(( A) = 2)
What is the English description of the interval?
● | ● | ● | ● |
A = 0 | A = 2 | A = 4 | A = 6 |
A = 0 ∧while A≠6 do (skip ∧ A := A + 2)
len(3) ∧ A = 0 ∧ A gets A + 2
A = 0 ∧ A gets A + 2 ∧halt(A = 6)
What is the English description of the interval?
● | ● | ● | ● | ● |
A = 0 | A = 2 | A = 0 | A = 2 | A = 0 |
len(4) ∧ A = 0 ∧ A gets 2 − A
((A = 0 ∧ A := 2 ∧skip) ; skip; |
(A = 0 ∧ A := 2 ∧skip) ; skip) |
∧fin(A = 0) |
What is the English description of the interval?
● | ● | ● | ● | ● |
A = 0 | A = 0 | A = 2 | A = 2 | A = 2 |
(skip ∧ A = 0) ; skip ; (len(2) ∧ A = 2)
What is the English description of the interval?
From first order ITL to pictorial semantics
len(3) ∧ A = 1 ∧ A gets 2 + A
● | ● | ● | ● |
A = 1 | A = 3 | A = 5 | A = 7 |
What is the English description of the interval?
(A = 0 ∧ A := A + 4 ∧skip) ; (skip ∧ A := 0)
● | ● | ● |
A = 0 | A = 4 | A = 0 |
What is the English description of the interval?
halt(A = 0) ∧ A = 8 ∧ (skip ∧ A := A − 2)∗
● | ● | ● | ● | ● |
A = 8 | A = 6 | A = 4 | A = 2 | A = 0 |
What is the English description of the interval?