{-

Dijkstra's Dutch National Flag program.

Nite: post-condition is weak in that it does not impose that the
program does not change the array in any other way than permutating
it.

-}

prog ducthFlag (a::& Int[])

b,i,r:: Int ;
tmp  :: Int

pre   0 < #a  /\  allRWB a 

do

{ b:=0; i:=0; r := #a ;

  inv   allRWB a /\
       (!k :- k range from r to #a -: isRed   (a[k])) /\
       (!k :- k range from b to i  -: isWhite (a[k])) /\
       (!k :- k range from 0 to b  -: isBlue  (a[k])) /\
       (b range from 0 to (i+1))   /\
        i <= r		     /\
       	r <= #a

  metric r-i

  while i<r do
    if a[i]=2
      then { tmp := a[i]; a[i]:=a[b]; a[b]:=tmp ;
	     b:=b+1 ; i:=i+1 }
      else if a[i]=1
      then i:=i+1
      else { r:=r-1 ;
	     tmp := a[i]; a[i]:=a[r]; a[r]:=tmp }
}

post dutchSorted a 

lconst

allRWB		:: Int[] -> Bool	;
cntRed		:: Int[] -> Int		;
cntWhite	:: Int[] -> Int		;
cntBlue		:: Int[] -> Int		;
isRed		:: Int -> Bool		;
isWhite		:: Int -> Bool		;
isBlue		:: Int -> Bool		;
dutchSorted	:: Int[] -> Bool