达夫尼的实数是多少？

Question

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

Answer 1

Dafny 的 real 数字不是浮点数。

从验证的角度来看，它们是数学实数，Dafny 使用 Z3 的实数算术理论对它们进行推理。

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