1void __VERIFIER_assert(int cond) {
2 if (!(cond)) {
3 ERROR: goto ERROR;
4 }
5 return;
6}
7
8
9
10int array[5];
11int n=5;
12
13void SelectionSort()
14{
15 int lh, rh, i, temp;
16
17 for (lh = 0; lh < n; lh++) {
18 rh = lh;
19 for (i = lh + 1; i < n; i++)
20 if (array[i] < array[rh]) rh = i;
21 temp = array[lh];
22 array[lh] = array[rh];
23 array[rh] = temp;
24 }
25}
26
27int main(void){
28
29 int array[5],i;
30
31 for(i=5 -1; i>=0; i--)
32 array[i]=i;
33
34 SelectionSort();
35
36 for(i=0; i<5; i++)
37 __VERIFIER_assert(array[i]==i);
38
39}