acsl-examples/16_bubble_sort.c at master · evdenis/acsl-examples · GitHub

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
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133


#pragma JessieTerminationPolicy(user)


/*@
  predicate sorted{Here}(int* a, integer start_index, integer end_index) =
    \forall integer k1, k2;
    start_index <= k1 <= k2 <= end_index ==> a[k1] <= a[k2];
*/

/*@
  predicate swapped{L1,L2}(int* a, integer i, integer j) =
  \at(a[i],L1) == \at(a[j],L2) &&
  \at(a[j],L1) == \at(a[i],L2) &&
  \forall integer k; k != i && k != j
     ==> \at(a[k],L1) == \at(a[k],L2);
  */

/*@
  inductive IPermut{L1,L2}(int* a, integer index_start, integer end_start)
  {
  case Permut_refl{L}:
  \forall int* a, integer index_start, end_start;
  IPermut{L,L}(a, index_start, end_start);

  case Permut_sym{L1,L2}:
  \forall int* a, integer index_start, end_start;
  IPermut{L1,L2}(a, index_start, end_start) ==>
  IPermut{L2,L1}(a, index_start, end_start);

  case Permut_trans{L1,L2,L3}:
  \forall int* a, integer index_start, end_start;
  IPermut{L1,L2}(a, index_start, end_start) &&
  IPermut{L2,L3}(a, index_start, end_start) ==>
  IPermut{L1,L3}(a, index_start, end_start);

  case Permut_swap{L1,L2}:
  \forall int* a, integer index_start, end_start, i, j;
  index_start <= i <= end_start && index_start <= j <= end_start &&
  swapped{L1,L2}(a, i, j) ==>
  IPermut{L1,L2}(a, index_start, end_start);
  }
  */


/*@
  requires \valid(t+i) && \valid(t+j);
  //assigns t[i],t[j];
  ensures \forall integer k;
	0 <= k < n && k != i && k != j ==> t[k] == \old(t[k]);
  ensures swapped{Old,Here}(t,i,j);
  */
void sort_swap3(int t[], int i, int j, int n) {
  int tmp = t[i];
  t[i] = t[j];
  t[j] = tmp;
}

/*@
  requires 0 < length;
  requires \valid(a+(0..length-1));
  //assigns a[0..length-1];
  behavior sorted:
		ensures sorted(a, 0, length-1);
  behavior permutation:
		ensures IPermut{Old,Here}(a, 0, length-1);
*/
void bubble_sort(int* a, int length)
{
	int up = 1;
	int down;
	int fixed_up = up;

	/*@
   // loop assigns a[0..up-1];
		for sorted:
			loop invariant fixed_up == up;
			loop invariant 0 < up <= length;
			loop invariant sorted(a, 0, up-1);
			loop invariant \forall integer k;
				up < k < length ==> a[k] == \at(a[k], Pre);
		for permutation:
			loop invariant IPermut{Pre,Here}(a, 0, length-1);
	*/
	for (; up < length; up++, fixed_up = up)
	{
		//@ for sorted: assert sorted(a, 0, up-1);
    //@ for permutation: assert IPermut{Pre,Here}(a, 0, length-1);
		fixed_up = up;
		down=up;
		//@ for sorted: assert sorted(a, down, up);
    //@ assert down < length;
		/*@
     //  loop assigns a[down+1..up];

			for sorted:
				loop invariant fixed_up == up;
        loop invariant 0 <= down < length;
				loop invariant 0 <= down <= up < length;
				loop invariant sorted(a, 0, down-1);
				loop invariant sorted(a, down, up);
				loop invariant \forall integer k;
					up < k < length ==> a[k] == \at(a[k], Pre);
				loop invariant  0 < down < up ==> a[down-1] <= a[down+1];
			for permutation:
				loop invariant IPermut{Pre,Here}(a, 0, length-1);
		*/
		while (0 < down && a[down] < a[down-1] )
		{
      //@ for permutation: assert IPermut{Pre,Here}(a, 0, length-1);
		  //@ for sorted: assert sorted(a, 0, down-1);
		  //@ for sorted: assert sorted(a, down, up);
		  //@ for sorted: assert a[down] < a[down-1];

		  sort_swap3(a,down,down-1, length);
		  //@ for permutation: assert IPermut{Pre,Here}(a, 0, length-1);
		  //@ for sorted: assert a[down-1] <= a[down];
			//@ for sorted: assert sorted(a, 0, down-2);
			//@ for sorted: assert sorted(a, down, up);
			// ==>

			//@ for sorted: assert sorted(a, down-1, up);
			down = down-1;
			//@ for sorted: assert sorted(a, 0, down-1);
			//@ for sorted: assert sorted(a, down, up);
			 //@ for permutation: assert IPermut{Pre,Here}(a, 0, length-1);
		}
		//@ for sorted: assert sorted(a, 0, up);
     //@ for permutation: assert IPermut{Pre,Here}(a, 0, length-1);
	}
   //@ for permutation: assert IPermut{Pre,Here}(a, 0, length-1);
}