docs: public static /*@pure@*/ double info(int counts[]) {
      
      int total = 0;
      double x = 0;
      for (int j = 0; j < counts.length; j++) {
        x -= xlogx(counts[j]);
        total += counts[j];
      }
      return x + xlogx(total);
    }