Sort an array A of 0s and 1s so the 0s come before the 1s

// Sort an array A of 0’s and 1’s so the 0’s come before the 1’s
// using swapping. The size of the array is n.
int bitsort(int *A, int n) {

int i=0;
int j=n-1;
while( i < j ) {
if( A[i] == 0 ) {
++i;
} else if( A[j] == 1 ) {
--j;
} else {
swap( A[i], A[j] );
}
}

return j;

(b) State and prove a loop invariant for the while-loop that you can use to establish the correctness of your code.

(c) Prove that the correctness of your code follows from the loop invariant and the termination condition of the loop.

(d) Under what conditions does your code return the number of 0’s in the input array?

Solution

Loop invariant:
-----------------
All Elements to the left of i are 0
and All Elements to the right of j are 0

Proof:
------
1)   Initial condition:       When loop begins value of i is 0 and value of j is n-1
2)   Iterative condition:    I get incremented only when arr[i] is 0 and j gets decremented only when arr[j] is 1
                           This keeps loop invariant intact keeping all elements to left of i as 0 and to the right of j as 1.
3)   Terminal condition:       Loop terminates when i == j, in that case array is sorted.

This invariant helps successfully sort the bit array

we know that After loop terminates, i is equal to the number of 0\'s in array
This function returns j
so, this function returns number of 0\'s when i is equal to j