jdk/src/share/classes/java/util/stream/Streams.java
changeset 20507 8498104f92c3
parent 19800 6e1fef53ea55
child 22297 1c62c67d9dd2
--- a/jdk/src/share/classes/java/util/stream/Streams.java	Wed Oct 02 19:13:42 2013 -0400
+++ b/jdk/src/share/classes/java/util/stream/Streams.java	Wed Oct 02 16:34:12 2013 +0200
@@ -169,7 +169,9 @@
 
         private int splitPoint(long size) {
             int d = (size < BALANCED_SPLIT_THRESHOLD) ? 2 : RIGHT_BALANCED_SPLIT_RATIO;
-            // 2 <= size <= 2^32
+            // Cast to int is safe since:
+            //   2 <= size < 2^32
+            //   2 <= d <= 8
             return (int) (size / d);
         }
     }