Is Dijkstra Wrong? Another look at the Dutch National Flag problem

The Dutch National Flag problem was invented by W.H.J.Feijen[1]. The problem may be phrased as follows[2]

Given `N’ objects coloured red, white or blue, sort them so that objects of the same colour are adjacent, with the colours in the order red, white and blue.

The Solution

The simplest solution is to use three arrays- put all the reds in the first array, whites in second one and so on -and concatenate the results. Here we assume that that is not acceptable and that the array has to be rearranged in-place.

Dijkstra’s solution is given below:

begin 
  glovar buck; 
  glocon N;
  privar r,w,b;
  r vir int, w vir int, b vir int = 1,N,N
  do w>= r ->
      begin
        pricon col;
        col vir colour := buck[w]
        if col == red -> buck:swap(r,w); r := r+1
         ||col == white -> w := w-1
         ||col == blue  -> buck:swap(b,w); w := w-1; b := b-1
         fi
      end
  od  
end           

Here buck, short for bucket, is the array of N objects with index ranging from 1 to N. Some key words that are not so common:

• glovar: variable whose scope includes the current block and can be modified
• glocon: variable whose scope includes the current block and cannot be modified
• privar: variable whose scope is the current block
• pricon: constant whose scope is the current block
• vir: virgin (uninitialised) variable/constant

Informal Proof of Correctness

Consider the following predicate, known as the loop invariant:

    buck(i) == red    if 1 <= i < r
            == white  if w < i <= b
            == blue   if b < i <= N

Initially the loop invariant is vacuously true. Convince yourself that the loop invariant holds at the beginning and end of every subsequent iteration.

The terminating condition is (w-r)<0. Notice that (w-r) is initially N-1 and is reduced by one at very iteration and hence when it attains the value -1 the iterative loop terminates. Given the loop invariant continues to hold we can conclude that at the end of the program we have:

    buck(i) == red    if 1 <= i < r
            == white  if r <= i <= b
            == blue   if b < i <= N

which is what we set out achieve.

Applications of the Algorithm

One of the most common applications of this algorithm is to partition an array. Consider an array of numbers A. Define

    Colour(A[i]) = red if A[i] < x
                    = white if A[i] == x
                    = blue if A[i] > x

The above algorithm now partitions A such that all values > x follow all values == x which in turn follow all values < x. If on the other hand we define

    Colour(A[i]) =  = white if A[i] < x
                    = blue if A[i] >= x

then we partition A into two sets with all values >= x following all values < x. This sort of partitioning is used in the Quicksort algorithm and in median finding

Optimisation

Notice that in the above algorithm if the entire array consists only of whites there will be no swaps. If it consists only of blues there will N identity swaps; swaps of the kind buck:swap(x,x) and hence near zero cost. If it consists only of reds there will N-1 real swaps and one identity swap. To avoid these redundant swaps the author suggests the following program:

begin 
  glovar buck; 
  glocon N;
  privar r,w,b;
  r vir int, w vir int, b vir int = 1,N,N
  do w>= r ->
      begin
        privar colr;
        colr vir colour := buck[r]
        do colr == red and r < w -> r:=r+1; colr = buck[r] od
        begin
            glovar buck,r,w,b
            glocon colr;
            privar colw;
            colw vir colour := buck[w]
            do colw == white and w > r+1 -> w:=w-1; colw:=buck[w] od
        
            if colw == red -> buck:swap(r,w); r := r+1
             ||colw == white -> w := w-1
             ||colw == blue  -> buck:swap(b,w); w := w-1; b := b-1;
                               buck:swap(r,w) 
             fi
         end
         if colr == white -> w:=w-1
          ||colr == blue -> buck:swap(b,w); w := w-1; b := b-1
         fi 
      end
  od  
end           

The loop invariant mentioned earlier holds in this case as well. In addition it holds at Line 11 and at Line 17. At Line 23, buck[r] has move to buck[w] while maintaining the loop invariant and at Line 26, w has been reduced by 1 while still maintaining the invariant. This algorithm performs no swaps or just identity swaps, as defined earlier, if the entire array is white or red. Notice that in general this algorithm uses fewer swaps than in the previous case but it does not reduce the big-Oh complexity.

The author claims that there are only two possibilities for colr: white or blue at Line 11. Hence at Line 24 colr == red is never checked. This is not correct as it is possible that colr == red when r == w. Admittedly, the missing statement is:
|| colr == red -> skip;

The issue with not adding that statement is that according to the semantics of the language proposed by the author, if none of the guards in an if statement are true then the program should abort.

References
1 Dijkstra, E.W “A Discipline of Programming,” Prentice Hall 1976, Chapter 14.
2 http://www.csse.monash.edu.au/~lloyd/tildeAlgDS/Sort/Flag/