```// ************************************************************************** //
//                                                                            //
//    eses                   eses                                             //
//   eses                     eses                                            //
//  eses    eseses  esesese    eses   Embedded Systems Group                  //
//  ese    ese  ese ese         ese                                           //
//  ese    eseseses eseseses    ese   Department of Computer Science          //
//  eses   eses          ese   eses                                           //
//   eses   eseses  eseseses  eses    University of Kaiserslautern            //
//    eses                   eses                                             //
//                                                                            //
// ************************************************************************** //
// SelectionSort determines in iteration i the the minimum b[imin] of the     //
// still unsorted array b[i..aSize-1]. After this, b[i] and b[imin] are       //
// swapped, so that b[0..i] is then already sorted, and the procedure is      //
// repeated for searching the minimum of b[i+1..aSize-1] until the entire     //
// array is sorted. Clearly, a variant is to search the maximum and put it    //
// on the rightmost border of the then unsorted left part.                    //
// ************************************************************************** //

macro aSize = 16;
macro iSize = 64;

module SelectionSort([aSize]int{iSize} ?a,b, event !ready) {
nat{aSize} imin;
for(i=0..(aSize-1))
b[i] = a[i];
for(i=0..(aSize-1)) {
// find the minimum b[imin] of b[i..aSize-1]
imin = i;
for(j=i+1..(aSize-1)) {
if(b[j] < b[imin])
next(imin) = j;
pause;
// here, b[imin] is the minimum of b[i..j]
assert(forall(k=i..j) (b[imin]<=b[k]));
}
// swap b[i] with b[imin]
next(b[i]) = b[imin];
next(b[imin]) = b[i];
pause;
// an invariant is here that b[0..i] is already sorted
assert(forall(k=1..i) (b[k-1]<=b[k]));
}
}
drivenby Test01 {
for(i=0..aSize-1) a[i] = i;
for(i=0..aSize-1) assert(b[i] == i);
}
drivenby Test02 {
for(i=0..aSize-1) a[i] = aSize-1-i;