dafny建模整数溢出

问题描述

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

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

我想念什么？

解决方法

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的相对较新的功能（好吧，不是最近的，但在过去的几年中），根据我的经验，除非您特别考虑一段代码进行按位运算（例如加密货币）。我建议尽可能避免使用位向量。