Dafny中的实数是什么？

Question

Dafny中的实数是什么？它们是否表示为IEEE 754-2008浮点数？如果不是，那是什么呢？也就是说，在Dafny中真实类型的规范是什么？

Answer 1

达夫尼的real数不是浮点数。

从验证的角度来看，它们是数学实数，并使用Z3的实数理论对它们进行了愚蠢的推理。

从编译的角度来看，Dafny实际上将它们编译成BigRationals，这是因为Dafny没有任何用于创建无理实数的内置操作。