by manual
l0 | t1 | l1: | x = x ∧ y = y ∧ z = −1 | |
l1 | t2 | l2: | −5 ≤ x ∧ x = x + z ∧ y = 0 ∧ z = z − 1 | |
l2 | t3 | l2: | y < x ∧ x = x ∧ y = y + 1 ∧ z = z | |
l2 | t4 | l1: | x ≤ y ∧ x = x ∧ y = y ∧ z = z |
The following invariants are asserted.
l0: | TRUE |
l1: | z < 0 |
l2: | z < −1 |
The invariants are proved as follows.
0 | (l0) | TRUE | ||
1 | (l1) | z < 0 | ||
2 | (l2) | z < −1 | ||
3 | (l2) | z < −1 | ||
4 | (l1) | z < −1 |
3 | → 2 | |
4 | → 1 |
0 | t1 1 | |
1 | t2 2 | |
2 | t3 3 | |
2 | t4 4 |
l2 | e | : | x = x ∧ y = y ∧ z = z |
We consider subproblems for each of the 1 SCC(s) of the program graph.
Here we consider the SCC {
, }.We remove transition
using the following ranking functions, which are bounded by −5.: | x |
: | x |
We consider subproblems for each of the 1 SCC(s) of the program graph.
Here we consider the SCC {
}.We remove transition
using the following ranking functions, which are bounded by 0.: | x − y |
There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.
manual