确定Java中Math.Ranb()输出的上限

如果能有真知灼见或方法来正式证明此值表示IEEE754浮点表示中小于1.0的最大数，我会非常感激.

作为一个词，Java有很多含义.在很多方面，它"只是"一个规范，而不是一个实现.那么，如何证明Math.random()函数可以做到这一点呢？好吧，这取决于你所说的Java是什么意思，但主要是not possible，我们需要深入研究"直到但不包括1.0"是什么意思.幸运的是，实际的JDK21源代码的javadoc明确包含以下API说明:

     * @apiNote
     * As the largest {@code double} value less than {@code 1.0}
     * is {@code Math.nextDown(1.0)}, a value {@code x} in the closed range
     * {@code [x1,x2]} where {@code x1<=x2} may be defined by the statements

相反，这表明，实际上，它can产生的最大值是Math.nextDown(1.0)，这锁定了"最高但不包括1.0"的含义.不幸的是，API注释不是规范的一部分.这仅仅是提示性的.

因此，在谈到问题的实质之前，我们需要对两点含糊其辞:

• Java actually并不完全保证完美的IEEE754数学；这就是关键字strictfp存在的原因，但据我所知，它对您可能遇到的任何现代体系 struct /OS/JVM-Release组合没有任何作用，而且它都是IEEE754.请注意，所有这些库方法(如Math.random())都是not strictfp.所以，这并不重要，这很好.尽管如此，如果你问我如何正式证明Java规范保证Math.random()在符合规范的实现上可能生成的最大数字是IEEE754双精度数，它是所有小于1.0的数字中最大的一个？答案是you cannot do that.我们必须假定"一个使用实际IEEE754数学运算的JDK".

在我们添加警告的同时，让我们回避整个API文档，这些词是什么意思，直接说:让我们分析一下the current code does: java.util.Random source code as of 2024-03-07:

第697-700行:

  @Override
    public double nextDouble() {
        return (((long)(next(Double.PRECISION - 27)) << 27) + next(27)) * DOUBLE_UNIT;
    }

这是我们需要分析的关键代码.注:

• next(int)返回随机位序列-int参数表示要返回多少位.例如，next(2)以相等的概率返回:0、1、2或3.
• 正如人们可能预料的那样，Double.PRECISION是‘53’--它表示专用于有效数的IEEE754双精度数中的位数.请参见wikipedia on IEEE754.

整个代码可以归结为一个简单得多的理解:

return next(53) * DOUBLE_UNIT;

那么，它为什么要做这个奇怪的歌舞 routine ，它生成26个随机位，将它们左移27个，然后再生成27个随机位？因为next返回int，所以他们必须进行2个调用，而代码决定只将53除以中间.这是一种分散注意力的方式，不会影响数学运算，因此，它只是:生成‘有效位’量的随机比特，然后将其乘以Double_UNIT，即:

    private static final double DOUBLE_UNIT = 0x1.0p-53; // 1.0 / (1L << 53)

现在让我们假设:

• 我们信任next(int)，因为我们相信它做到了它所说的事情，并且它返回的每一位确实完全有可能是一个‘1’位，就像它是一个没有依赖关系的‘0’位一样(现在生成的位具有零预测值，以try 预测它将生成的下一个位).

然后，我们有一个long形式的数字，在0到2^53-1之间，均匀分布.我们现在将这个数字乘以double和1.0/2^53).如果我们忘记IEEE754和所有这些，这确实得到了一个介于0和1之间的数字，具体地说，有2^53个不同的选项，从0/2^53，也就是0，一直到最多(2^53-1)/2^53，它比1.0小得非常非常小，正好比它小1/2^53.

现在将IEEE754带回来:Java将在进行数学运算之前将那个长度静默地转换为一个双精度数(因为唯一可以做到这一点的字节码是DMUL，您可以编写这段代码，让javac编译它，然后运行javap进行判断:实际上，为此生成的操作码是L2D(长2双精度)，然后是DMUL(乘2双精度加在一起).

这是"安全的"吗？IEEE754的答案是肯定的:有效位是53位，所以一个可以用53位表示的数字将会"适合"，而不会损失任何转换.字节码L2D会不会毫无损失地做到这一点？如果Java只是一堆规范文档，我不知道如何才能正式地证明这一点.文档建议这样做，我所能接触到的所有JVM实现都是按照您的预期来做的.

我们现在到了DMUL，我们又一次被困住了，无法正式证明任何东西，因为DMUL所做的事情的定义是Java Virtual Machine Specification §6.5.dmul--那是一堆英文文本.但该规范确实表示，它受IEEE 754算术规则的管辖，如果出现舍入，则引用§2.8(它不应符合IEEE 754规则).

我们需要在这里进行规范到形式的飞跃，阅读IEEE754定义的内容，并相信我们的JVM实现了IEEE754所说的precisely.这就是它的工作方式:DMUL几乎只会请求CPU来做这件事；JVM实现满足了遵循IEEE754到底层体系 struct 的要求.这就是strictfp存在原因:如果伪装是不精确的，因为已知底层体系 struct 实际上并不执行IEEE754数学运算，那么JVM需要通过费力地应用IEEE754本身而不是使用CPU的操作码来实现速度要慢数百倍的DMUL，这是不值得的，所以strictfp作为安全阀存在:JVM将只是请求CPU来做这件事，除非您使用strictfp，在这种情况下，不能相信CPU会完全正确地完成它，否则它不会.除非所有CPU都完全正确，所以strictfp什么都不做，或者OpenJDK不关心，strictfp什么也不做，因为没有人会被激怒.在这方面我帮不了你，规格也帮不了你.

现在，我们需要深入研究英特尔、AMD、苹果的芯片设计团队、亚马逊的设计团队(他们也拥有运行JVM的基于ARM的芯片)，等等，他们在实现CPU方面promise 了什么.

但是，假设它是"我们遵循IEEE754,exactly"，我们可以看看IEEE754规定的是什么，这很容易:以前11位(64-53 = 11)作为零开始的长整型将无损失地转换为双精度型，并且这样的双精度型可以被DOUBLE_UNIT(1/2^53)无损失地除以.

让我们‘伪装’它并编写此代码，强制生成可能的最大值:

import java.util.*;

class Test {
  public static void main(String[] args) {
    Random r = new Random() {
      protected int next(int bits) {
        // return all 1-bits
        int x = 1 << bits;
        return x - 1;
      }
    };
    double v = r.nextDouble();
    System.out.printf("%f -> %X equal to nextDown? %s %s\n",
       v, Double.doubleToLongBits(v),
       v == Math.nextDown(1.0) ? "YES!" : "NO",
       v == 1.0 ? "1-exactly" : "not-1");
  }
}

无论如何，这在我的JVM/ARCH/OS组合上都会尽职尽责地报告:

1,000000 -> 3FEFFFFFFFFFFFFF equal to nextDown? YES! not-1

注意，它在%f中将Math.nextDown(1.0)四舍五入到1.0，但是，正如字符串print所示，它不是1.0.我们见证了这样一个事实，没有说明符的%f将应用少量舍入，而不是任何基本的东西，例如见证Math.random()可以生成实际的文字1.0.