blob: 5cad03d71aeda5ccb230f8c0b5d00bdf97054da9 (
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
|
// Example from Cousot Habwachs POPL 1978
// Bubble sort, where array operations are abstracted away
// to get a non-deterministic scalar program
// expected results:
// - with polyhedra, no assertion failure (proof of absence of array overflow)
// - with intervals, assertion failure
int B,J,T;
int N = rand(0,100000); // array size
B = N;
while (B >= 1) {
J = 1;
T = 0;
while (J <= B-1) {
// array bound-check
assert(1 <= J && J <= N);
assert(1 <= (J+1) && (J+1) <= N);
// the non-deterministic test models comparing TAB[J] and TAB[J+1]
if (rand(0,1)==0) {
// where, we would exchange TAB[J] and TAB[J+1];
T = J;
}
J = J + 1;
}
B = T;
}
|
