dafny 建模整数溢出答案

【问题标题】：dafny modeling integer overflowdafny 建模整数溢出
【发布时间】：2020-09-16 08:14:22
【问题描述】：

Dafny 模型整数会溢出吗？当 Dafny 证明以下内容时，我感到很惊讶：

method overflow(c : int)
{
    if (c > 0)
    {
        assert((c+1) > 0);
    }
}

我错过了什么？

【问题讨论】：

【解决方案1】：

Dafny 中的类型int 表示“数学整数”。所以没有溢出。

如果你想对机器算术建模，有几种方法可以做到。

一种方法是定义如下内容：

type uint64 = x:int | 0 <= x < 0x10000000000000000

然后当您尝试将结果存储在 uint64 中时，您将收到错误消息：

method overflow(c: uint64) {
  if c > 0 {
    var d: uint64 := c + 1;
    assert d > 0;
  }
}

此技术主要用于证明您的程序不会溢出。相反，如果您想推理一个有意使用二进制补码算法的程序，您可以使用位向量来做到这一点，如下所示：

method overflow(c: bv64) {
  if c > 0 {
    assert c + 1 > 0;
  }
}

位向量是 Dafny 的一个相对较新的补充（好吧，不是最近，但在过去几年中），根据我的经验，它们没有被广泛使用，除非您专门推理一段执行按位运算的代码（例如，加密）。如果可能的话，我会建议远离位向量。

【讨论】：

我有一个场景，我实际上想要整数溢出，我使用位向量对其进行编码，那里似乎有一个错误（？）这是永久链接： rise4fun.com/Dafny/cMPs 这是我能想到的最短的例子：method wrong(a : bv32, b : bv32){if ((a >= 1) || (b >= 1)) { return; } assert (a+b <= 0);} dafny 不会在事实上可能发生的断言违规上发出警告。
我认为位向量在 Dafny 中是无符号的。因此，您发送的示例是正确的，因为 a 和 b 如果小于 1，则它们都必须为 0。
是的，Dafny 中的位向量是无符号的。对它们的算术运算将换行。