Selection Sort, Java version
Sorting an array of integers in increasing order, by iterative selection of the minimum element
Authors: Claude Marché
Topics: Array Data Structure / Permutation / Sorting Algorithms / Inductive predicates
Tools: Krakatoa
References: The VerifyThis Benchmarks
See also: Insertion Sort, C version / Selection Sort, C version
see also the index (by topic, by tool, by reference, by year)
/*@ predicate Sorted{L}(int a[], integer l, integer h) =
@ \forall integer i j; l <= i <= j < h ==> a[i] <= a[j] ;
@*/
/*@ predicate Swap{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 Permut{L1,L2}(int a[], integer l, integer h) {
@ case Permut_refl{L}:
@ \forall int a[], integer l h; Permut{L,L}(a, l, h) ;
@ case Permut_sym{L1,L2}:
@ \forall int a[], integer l h;
@ Permut{L1,L2}(a, l, h) ==> Permut{L2,L1}(a, l, h) ;
@ case Permut_trans{L1,L2,L3}:
@ \forall int a[], integer l h;
@ Permut{L1,L2}(a, l, h) && Permut{L2,L3}(a, l, h) ==>
@ Permut{L1,L3}(a, l, h) ;
@ case Permut_swap{L1,L2}:
@ \forall int a[], integer l h i j;
@ l <= i <= h && l <= j <= h && Swap{L1,L2}(a, i, j) ==>
@ Permut{L1,L2}(a, l, h) ;
@ }
@*/
class Sort {
/*@ requires t != null &&
@ 0 <= i < t.length && 0 <= j < t.length;
@ assigns t[i],t[j];
@ ensures Swap{Old,Here}(t,i,j);
@*/
void swap(int t[], int i, int j) {
int tmp = t[i];
t[i] = t[j];
t[j] = tmp;
}
/*@ requires t != null;
@ behavior sorted:
@ ensures Sorted(t,0,t.length);
@ behavior permutation:
@ ensures Permut{Old,Here}(t,0,t.length-1);
@*/
void selection_sort(int t[]) {
int i,j;
int mi,mv;
/*@ loop_invariant 0 <= i;
@ for sorted:
@ loop_invariant Sorted(t,0,i) &&
@ (\forall integer k1 k2 ;
@ 0 <= k1 < i <= k2 < t.length ==> t[k1] <= t[k2]) ;
@ for permutation:
@ loop_invariant Permut{Pre,Here}(t,0,t.length-1);
@ loop_variant t.length - i;
@*/
for (i=0; i<t.length-1; i++) {
// look for minimum value among t[i..n-1]
mv = t[i]; mi = i;
/*@ loop_invariant i < j && i <= mi < t.length;
@ for sorted:
@ loop_invariant mv == t[mi] &&
@ (\forall integer k; i <= k < j ==> t[k] >= mv);
@ for permutation:
@ loop_invariant Permut{Pre,Here}(t,0,t.length-1);
@ loop_variant t.length - j;
@*/
for (j=i+1; j < t.length; j++) {
if (t[j] < mv) {
mi = j ; mv = t[j];
}
}
Before:
swap(t,i,mi);
//@ for permutation: assert Permut{Before,Here}(t,0,t.length-1);
}
}
}