在 dafny 中获取指数

问题描述 投票:0回答:0

我是 dafny 的新手,我在获取整数的指数时遇到了麻烦

不变量 x >= 0 && y >= 0 && ((x + y) * (2^(u-1)) + 结果 == i1 + i2);

对于说“2^(u-1)”的部分,我一直收到错误提示,它期望使用位向量,但却得到了 int。我该如何解决?我需要结果是一个 int

dafny bitvector loop-invariant
© www.soinside.com 2019 - 2024. All rights reserved.