```// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// ShellSort [Shel59,Cyph89,PlPS92,Sedg96,JiLV00,Ciur01] is a variant of      //
// InsertionSort. It performs InsertionSort on h-sequences b[0],b[h],b[2h],...//
// of the array b and repeats this for smaller h until h=1 (so that in this   //
// last step an InsertionSort is made). It is to be noted that a h-sorted     //
// sequence remains h-sorted when sorting by another step h' is done later.   //
// The performance of ShellSort depends on the chosen set of numbers h (see   //
// [Ciur01]), where theoretically any sequence can be used that ends with h=1.//
// Donald Shell proposed the sequence h=1,2,4,8,... which is however not      //
// that good. A better sequence is h=1,3,7,15,31,... (i.e. h_i = 2^i-1) for   //
// which Knuth proved the worst case complexity O(n^1.5) which cannot be      //
// improved due to Prat. Another often used sequence is h=1,4,13, (i.e.       //
// h_{i+1} = 3*h_i+1). Pratt proved 1971 that h=1,2,3,4,6,9,8,12,18,27,..     //
// requires only O(n*(log(n))^2) steps where the sequence is obtained         //
// by adding 2*h_i and 3*h_i to the sequence if these numbers are not already //
// at the end of the sequence (i.e., h_i = 2^j*3^k for all j,k). Using this   //
// sequence and BubbleSort instead of InsertionSort, a sorting network can be //
// built with the same complexity of Batcher's bitonic sorter.                //
// ************************************************************************** //

[16] nat a;
[3] nat steps;

function ShellSort (nat aSize, sizeStep): nat {
nat i,j,h,s,t,v;

steps[0] = 7;
steps[1] = 3;
steps[2] = 1;

for(s=0..sizeStep-1) {
h = steps[s];
for(i=h..aSize-1) {
t = a[i];
j = i;
v = a[j-h];
while(j>=h & v>t) {
a[j] = v;
j = j-h;
if(j>=h)
v = a[j-h];
}
a[j]=t;
}
}
return 0;
}

nat k;
a[0] = 9;
a[1] = 8;
a[2] = 16;
a[3] = 15;
a[4] = 1;
a[5] = 10;
a[6] = 2;
a[7] = 11;
a[8] = 3;
a[9] = 4;
a[10] = 6;
a[11] = 5;
a[12] = 14;
a[13] = 12;
a[14] = 7;
a[15] = 13;

k = ShellSort(16,3);
}

nat t,i;
bool test1_passed;

for(i=0..15){
a[i]=i+1;
}
a[5]=9;
a[8]=6;
a[10]=7;
a[6]=11;
test1_passed = true;

t = ShellSort(16,3);

for(i=0..15){
if((a[i]==(i+1)) & (test1_passed != false)){
test1_passed = true;
}else{
test1_passed = false;
}
}

}

nat t, i;
bool test2_passed;

for(i=0..15){
a[i]=i+1;
}
test2_passed = true;
t = ShellSort(16,3);

for(i=0..15){
if((a[i]==(i+1)) & (test2_passed != false)){
test2_passed = true;
}else{
test2_passed = false;
}
}
}

nat t, i;
bool test3_passed;

for(i=0..15){
a[i]=16-i;
}
test3_passed = true;
t = ShellSort(16,3);

for(i=0..15){
if((a[i]==(i+1)) & (test3_passed != false)){
test3_passed = true;
}else{
test3_passed = false;
}
}

}

```