blob: dd12e1ad258ac754094836993c60e8ead59a7718 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
|
// Example from Cousot Habwachs POPL 1978
// Heap sort, where array operations are abstracted away
// to get a non-deterministic scalar program
// expected results: with polyhedra, no assertion failure
int L,R,I,J;
int N = rand(1,100000); // array size
L = N/2 + 1;
R = N;
if (L >= 2) {
L = L - 1;
// model the assignment "K = TAB[L]"
assert(1 <= L && L <= N);
}
else {
// model the assignments "K = TAB[R]; TAB[R] = TAB[1]"
assert(1 <= R && R <= N);
assert(1 <= 1 && 1 <= N);
R = R - 1;
}
while (R >= 2) {
I = L;
J = 2*I;
while (J <= R && rand(0,1)==0) {
if (J <= R-1) {
// model the comparison "TAB[J] < TAB[J+1]"
assert(1 <= J && J <= N);
assert(1 <= (J+1) && (J+1) <= N);
if (rand(0,1)==0) { J = J + 1; }
}
// model the comparison "K < TAB[J]"
assert(1 <= J && J <= N);
if (rand(0,1)==0) {
// model the assignment "TAB[I] = TAB[J]"
assert(1 <= I && I <= N);
assert(1 <= J && J <= N);
I = J;
J = 2*J;
}
}
// model the assignment "TAB[I] = K"
assert(1 <= I && I <= N);
if (L >= 2) {
L = L - 1;
// model the assignment "K = TAB[L]"
assert(1 <= L && L <= N);
}
else {
// model the assignments "K = TAB[R]; TAB[R] = TAB[1]"
assert(1 <= R && R <= N);
assert(1 <= 1 && 1 <= N);
R = R - 1;
}
// model the assignment "TAB[1] = K"
assert(1 <= 1 && 1 <= N);
}
|
