// ************************************************************************** // // // // 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])); } emit(ready); } drivenby Test01 { for(i=0..aSize-1) a[i] = i; dw: await(ready); for(i=0..aSize-1) assert(b[i] == i); } drivenby Test02 { for(i=0..aSize-1) a[i] = aSize-1-i; dw: await(ready); for(i=0..aSize-1) assert(b[i] == i); } drivenby Test03 { for(i=0..aSize-1) a[i] = ((i%2==0)?i:((aSize%2==0)?aSize-i:aSize-1-i)); dw: await(ready); for(i=0..aSize-1) assert(b[i] == i); }