如何解决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的相对较新的功能(好吧,不是最近的,但在过去的几年中),根据我的经验,除非您特别考虑一段代码进行按位运算(例如加密货币)。我建议尽可能避免使用位向量。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。