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 {
, }.The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
x = x ∧ y = y ∧ z = z :
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
x = x ∧ y = y ∧ z = z :
The new variable xs is introduced. The transition formulas are extended as follows:
: | xs = xs |
: | xs = xs |
: | xs = xs |
: | xs = xs |
: | xs = x |
The new variable ys is introduced. The transition formulas are extended as follows:
: | ys = ys |
: | ys = ys |
: | ys = ys |
: | ys = ys |
: | ys = y |
The new variable zs is introduced. The transition formulas are extended as follows:
: | zs = zs |
: | zs = zs |
: | zs = zs |
: | zs = zs |
: | zs = z |
The following invariants are asserted.
l0: | TRUE |
l1: | TRUE |
l2: | 0 ≤ y |
: | x ≤ xs |
: | 0 ≤ y |
: | 0 ≤ y ∧ ys + x ≤ xs + y ∧ x ≤ xs |
: | 0 ≤ y ∧ −5 ≤ xs ∧ ys + x < xs + y ∧ ys < xs ∧ x ≤ xs ∨ 0 ≤ y ∧ −5 ≤ xs ∧ x < xs |
The invariants are proved as follows.
0 | (l0) | TRUE | ||
1 | (l1) | TRUE | ||
2 | (l2) | 0 ≤ y | ||
3 | ( | )0 ≤ y | ||
4 | ( | )0 ≤ y ∧ ys + x ≤ xs + y ∧ x ≤ xs | ||
5 | ( | )0 ≤ y ∧ −5 ≤ xs ∧ ys + x < xs + y ∧ ys < xs ∧ x ≤ xs | ||
6 | ( | )x ≤ xs | ||
7 | ( | )0 ≤ y ∧ −5 ≤ xs ∧ ys + x < xs + y ∧ ys < xs ∧ x ≤ xs | ||
8 | ( | )0 ≤ y ∧ −5 ≤ xs ∧ x < xs | ||
9 | ( | )0 ≤ y ∧ −5 ≤ xs ∧ x < xs |
7 | → 3 | |
9 | → 3 |
0 | t1 1 | |
1 | t2 2 | |
2 | t3 2 | |
2 | t4 1 | |
2 | e 3 | |
3 | 4 | |
4 | 5 | |
4 | 6 | |
5 | 7 | |
6 | 8 | |
8 | 9 |
We remove transition
using the following lexicographic ranking functions, which are bounded by [−5, 0].: | [x, x − y] |
: | [xs, xs − ys] |
: | [xs, xs − ys] |
: | [xs, xs − ys] |
There exist no SCC in the program graph.
manual