docs: public static /*@pure@*/ int[] sort(/*@non_null@*/ double[] array) {
  
      int[] index = new int[array.length];
      array = (double[])array.clone();
      for (int i = 0; i < index.length; i++) {
        index[i] = i;
        if (Double.isNaN(array[i])) {
          array[i] = Double.MAX_VALUE;
        }
      }
      quickSort(array, index, 0, array.length - 1);
      return index;
    }