Sorting indirectly

Initial State

The code below accomplishes the rearranging of the records from the ``indirectly sorted'' (by an array x of indices) array A.

 ;
while   do
	if  then ; 
	 else begin ;		
	           while  
			do ; 
		   ;
 	      end;

To prove correctness, observe that the invariant for the outer while loop is

and the invariant for the inner while loop is

• About this document ...