Dijkstra's Dutch Flag, Java version
The famous Dutch Flag examples due to Dijkstra. It aims at sorting an array of three colors blue, white and red.
Authors: Claude Marché
Topics: Historical examples / Array Data Structure
Tools: Krakatoa
See also: Dijkstra's national flag
see also the index (by topic, by tool, by reference, by year)
//@+ CheckArithOverflow = no
/*@ predicate is_color(integer c) =
@ c == FlagStatic.BLUE || c == FlagStatic.WHITE || c == FlagStatic.RED ;
@*/
/*@ predicate is_color_array{L}(int t[]) =
@ t != null &&
@ \forall integer i; 0 <= i < t.length ==> is_color(t[i]) ;
@*/
/*@ predicate is_monochrome{L}(int t[],integer i, integer j, int c) =
@ \forall integer k; i <= k < j ==> t[k] == c ;
@*/
class FlagStatic {
public static final int BLUE = 1, WHITE = 2, RED = 3;
/*@ requires t != null && 0 <= i <= j <= t.length ;
@ behavior decides_monochromatic:
@ ensures \result <==> is_monochrome(t,i,j,c);
@*/
public static boolean isMonochrome(int t[], int i, int j, int c) {
/*@ loop_invariant i <= k &&
@ (\forall integer l; i <= l < k ==> t[l]==c);
@ loop_variant j - k;
@*/
for (int k = i; k < j; k++) if (t[k] != c) return false;
return true;
}
/*@ requires 0 <= i < t.length && 0 <= j < t.length;
@ behavior i_j_swapped:
@ assigns t[i],t[j];
@ ensures t[i] == \old(t[j]) && t[j] == \old(t[i]);
@*/
private static void swap(int t[], int i, int j) {
int z = t[i];
t[i] = t[j];
t[j] = z;
}
/*@ requires
@ is_color_array(t);
@ behavior sorts:
@ ensures
@ (\exists integer b r;
@ is_monochrome(t,0,b,BLUE) &&
@ is_monochrome(t,b,r,WHITE) &&
@ is_monochrome(t,r,t.length,RED));
@*/
public static void flag(int t[]) {
int b = 0;
int i = 0;
int r = t.length;
/*@ loop_invariant
@ is_color_array(t) &&
@ 0 <= b <= i <= r <= t.length &&
@ is_monochrome(t,0,b,BLUE) &&
@ is_monochrome(t,b,i,WHITE) &&
@ is_monochrome(t,r,t.length,RED);
@ loop_variant r - i;
@*/
while (i < r) {
switch (t[i]) {
case BLUE:
swap(t,b++, i++);
break;
case WHITE:
i++;
break;
case RED:
swap(t,--r, i);
break;
}
}
}
}