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); } } }