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
|
/* Selection sort */
//@ type intmset
//@ logic intmset mset(int t[],int i,int j) reads t[..]
/*@ requires \valid_index(t,i) && \valid_index(t,j)
@ assigns t[i],t[j]
@ ensures t[i] == \old(t[j]) && t[j] == \old(t[i])
@*/
void swap(int t[],int i,int j) {
int tmp = t[i];
t[i] = t[j];
t[j] = tmp;
}
/*@ predicate sorted(int t[],int i,int j) {
@ \forall int k; i <= k < j => t[k] <= t[k+1]
@ }
@*/
/*@ requires n >= 1 && \valid_range(t,0,n-1)
@ assigns t[0..n-1]
@ ensures sorted(t,0,n-1) && mset(t,0,n-1) == \old(mset(t,0,n-1))
@*/
void selection(int t[], int n) {
int i,j,min;
init:
/*@ // t[0..i-1] is already sorted
@ invariant
@ 0 <= i <= n-1 &&
@ sorted(t, 0, i-1) &&
@ mset(t,0,n-1) == \at(mset(t,0,n-1),init) &&
@ \forall int k; \forall int l; 0 <= k < i =>
@ i <= l < n => t[k] <= t[l]
@ loop_assigns
@ t[0..n-1]
@ variant
@ n - i
@*/
for (i=0; i < n-1; i++) {
/* we look for the minimum of t[i..n-1] */
min = i;
/*@ invariant
@ i+1 <= j <= n &&
@ i <= min < n &&
@ \forall int k; i <= k < j => t[min] <= t[k]
@ variant
@ n - j
@*/
for (j = i + 1; j < n; j++) {
if (t[j] < t[min]) min = j;
}
/* we swap t[i] and t[min] */
swap(t,min,i);
}
}
|
