// ************************************************************************** // // // // 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 // // // // ************************************************************************** // // This file implements the well-known insertion sort procedure. The main idea // is to sort prefixes x[0..i-1] of the array x[0..N-1] and then store x[i] in // a separate variable y so that all entries x[j+1..i-1] can be moved one place // to the right and y can be stored at x[j+1]. // Note in many textbooks the while loop has condition (j>=0 & x[j]>y) and // no other code than x[j+1]=y is put after the loop. However, if conjunction // is commutative (as in MiniC and Quartz unlike in C), then in case of j==0, // the evaluation of this condition will not stop after j>=0 is seen false, // and instead also x[j]>y is evaluated which leads to a runtime error. // ************************************************************************** // thread InsertionSort { [10]nat x; nat i,j,y; // first create a test array in reverse order for(i=0..9) { x[i] = 10-i; } // now apply insertion sort for(i=1..9) { y = x[i]; // for element x[i], find its place in j = i-1; // already sorted list x[0..i-1] while(j>0 & x[j]>y) { x[j+1] = x[j]; j = j-1; } // now j==0 or x[j]<=y if(x[j]>y) { // note that this implies j==0 x[j+1] = x[j]; x[j] = y; } else { // here we have x[j]<=y, so that y must be placed at j+1 x[j+1] = y; } } }