Which sorting technique is this code?

Question

Someone asked me to sort an array, which I did as follows. Now we're fighting over which sorting technique this is. He's classifying it as bubble after explaining me the different sorting techniques he knows about, but I think it's not! But it does sort!

C code:

void sort(void){

int a[9]={4,2,1,3,5,7,5,6,8};
int i,j,temp;

for(i=0;i<9;i++)
{
    for(j=0;j<i;j++)
    {
        if(a[j] > a[i])
        {
            temp = a[i];
            a[i] = a[j];
            a[j] = temp;
        }
    }

}

for(i=0;i<9;i++)
{
    printf("\n%d",a[i]);
}
}

This is bubble, according to me which he agrees to, but also classifies the former as the same. I mean there's got to be a name for that!

for(i=0;i<9;i++)
{
    for(j=0;j<8;j++)
    {
        if(a[j] > a[j+1])
        {
            temp = a[j+1];
            a[j+1] = a[j];
                a[j] = temp;
        }
    }    

}

Answer 1

It looks more like a variant of insertion sort to me. In fact, the key is to remark that after each step of the outer loop, the beginning of the array (up to index i-1) is sorted. Then, the inner loop will only do comparisons until j reaches the first index k where a[k]>a[i], which is the place where you want to insert a[i]. After that, you'll always (well not really always if there are duplicate elements) swap values, since a[k]<=a[k+1]<=...<=a[i-1], effectively moving the elements to the right after the insertion point, like in the canonical insertion sort. The code below contains annotations that formalize that reasoning so that it can be proved by the Frama-C tool (NB: the assertions are only there to help the tool complete the proofs, what really matters are the loop invariant).

/*@ predicate sorted{L}(int* a, int n) =
       \forall integer i,j; 0<=i<=j<n ==> a[i]<=a[j];
*/

/*@ requires \valid(a+(0..n-1));
    requires n > 0;
    assigns a[0..n-1];
    ensures sorted(a,n);
 */
void sort(int* a, int n) {

int i,j,temp;

/*@ loop invariant sorted(a,i);
    loop invariant 0<=i<=n;
    loop assigns i,j,temp,a[0..n-1];
    loop variant n-i;
 */
for(i=0;i<n;i++)
{
  /*@ loop invariant sorted(a,i);
      loop invariant 0<=j<=i;
      loop invariant \forall integer k; 0<=k<j ==> a[k] <= a[i];
      loop assigns j,temp,a[0..j-1],a[i];
      loop variant i-j;
  */
    for(j=0;j<i;j++)
    {
        if(a[j] > a[i])
        {
          //@ assert \forall integer k; 0<=k<j ==> a[k]<=a[i];
          //@ assert \forall integer k; j<=k<i ==> a[i]<a[k];
            temp = a[i];
            a[i] = a[j];
            a[j] = temp;
          //@ assert \forall integer k; 0<=k<j ==> a[k]<=a[j];
          //@ assert \forall integer k; j<=k<=i ==> a[j]<=a[k];
          //@ assert \forall integer k,l; 0<=k<=l<j ==> a[k]<=a[l];
          //@ assert \forall integer k,l; j<k<=l<i ==> a[k]<=a[l];
       }
    }

}
}