title: Quicksort partition algorithm loop invariants defined in partition method
body: <p>I implemented the partition method in the quicksort algorithm but i dont know if it satisfies the loop invariant that they were given to me.</p>
  
  <pre><code>    public class qs {
        private qs(){}
  
  /**
   * Sort an array in ascending order
   * @param arr array to sor  */
     public static void quickSort(int[] arr){
      qs(arr, 0, arr.length);
          }
  
  /**
           * Sort a region of an array in ascending order.
           * Elements outside the given region are unchanged.
           * requires: 0 &lt;= start &lt;= end &lt;= arr.length
           * @param arr   array to sort
           * @param start start of region (inclusive)
           * @param end   end of region (exclusive)
           */
          private static void qs(int[] arr, int start, int end){
              if (end &lt;= start+1){    //region of length 0 or 1
                  return;
              }
              int x = arr[start];
              int p = partition(arr, start+1, end, x);
                  //now swap arr[start] with arr[p-1]
              arr[start] = arr[p-1];
              arr[p-1] = x;
              qs(arr, start, p-1);
              qs(arr, p, end);
  
  
  
          }
  
          /**
           * Partition a region of an array.
           * Rearranges elements in region so that small ones
           *   all have smaller indexes than the big ones.
           * Elements outside the region are unchanged.
           * requires: 0 &lt;= start &lt;= end &lt;= arr.length
           * @param arr   array to partition
           * @param start start of region (inclusive)
           * @param end   end of region (exclusive)
           * @param x     pivot - "small" and "big" are &lt;x, &gt;=x.
           * @return      start index (inclusive) of big elements
           *              in region after partition.
           */
          private static int partition(
              int[] arr, int start, int end, int x)
          {
  
              int l = start-1 ;
              int r = end;
              while (true) {
                  while(++l&lt; r &amp;&amp; arr[l] &lt; x);
  
                      while(r-- &gt; l &amp;&amp; arr[r] &gt; x);// find smaller item
  
                      if(l &gt;= r) // if pointers cross,
                          break; // partition done
                          else  {
                          int temp;
                      temp = arr[l];
                      arr[l] = arr[r];
                      arr[r] = temp;
                  }
              }
              return l;
              }
  
  
          public static void main(String[] args) {
              int[] a = {15,8,4,8,9,6,4,1,2,5,6,4};
              quickSort(a);
              for (int i = 0; i &lt; a.length; i++){
                  System.out.print(" "+a[i]);
              }
          }
      }
  </code></pre>