```// ************************************************************************** //
//                                                                            //
//    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.
// ************************************************************************** //

[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;
}
}
}
```