Dijkstra’s Dutch Flag

Here is a code for the famous Dutch Flag algorithm due to Dijkstra, to sort an array of three colors only.

0pt class Flag { 
     
    public static final int BLUE = 1, WHITE = 2, RED = 3; 
     
    public static boolean isMonochromatic(int t[], int i, int j, int c) { 
        for (int k = i; k < j; k++) if (t[k] != c) return false; 
        return true; 
    } 
 
    private static void swap(int t[], int i, int j) { 
        int z = t[i]; 
        t[i] = t[j]; 
        t[j] = z; 
    } 
 
    public static void flag(int t[]) { 
        int b = 0; 
        int i = 0; 
        int r = t.length; 
        while (i < r) { 
            switch (t[i]) { 
            case BLUE:   
                swap(t,b++, i++); 
                break;             
            case WHITE:  
                i++;  
                break; 
            case RED:  
                swap(t,--r, i); 
                break; 
            } 
        } 
    } 
} 
  1. Define a predicate expressing that a given array contains only one particular given color. Use it to specify and prove the isMonochromatic method.
  2. Specify the flag method to express that the resulting array has colors in the order BLUE, WHITE and RED. Prove it using an appropriate loop invariant.
  3. Specify and prove an additional behavior, expressing that the resulting array is a permutation of the original one.
This document was translated from LATEX by HEVEA.