dafny建模整数溢出

Question

Dafny模型整数溢出？当达夫尼证明了以下情况时，我感到惊讶：

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

我遗漏了什么？

Answer 1

达夫尼中的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 (好的，不是最近的，但在过去的几年中)的一个相对较新的添加，在我的经验中，它们没有被广泛使用，除非您是专门地对一段代码进行按位操作(例如，密码)的推理。如果可能的话，我建议远离位向量。