英文:
Calculating integer exponents in dafny
问题
我对 Dafny 还不熟悉，我在获取整数的指数方面遇到了问题。
对于这部分写着 "2^(u-1)" 的地方，我一直得到一个错误，它期望位向量(bitvectors)但却得到整数。我应该如何修复这个问题？我需要 result 是一个整数。
英文:
I'm new to dafny and I am having trouble with getting exponents for integers
invariant x >= 0 && y >= 0 && ((x + y) * (2^(u-1)) + result == i1 + i2);
for the part that says "2^(u-1)" i keep getting the error that it is expecting bitvectors but instead got int. How do I fix this? I need result to be an int
答案1
得分: 1
Dafny没有幂运算符，因此^不表示指数运算，而是按位异或，这就是为什么它抱怨位向量的原因。
function pow(base: int, exp: nat): int {
if exp == 0 then 1 else base * pow(base, exp-1)
}
invariant x >= 0 && y >= 0 && (x + y) * pow(2, u-1) + result == i1 + i2;
Dafny在乘法方面有一些问题，因为显然乘法是不可决定的，所以它可能不会自动验证。您需要通过归纳来证明您的不变式是真实的，可能需要一些关于pow和您特定问题的引理。
英文:
Dafny does not have an exponent operator so ^ is not exponentiation but instead bitwise xor, which is why it complaining about bit vectors.
function pow(base: int, exp: nat): int {
if exp == 0 then 1 else base * pow(base, exp-1)
}
invariant x >= 0 && y >= 0 && (x + y) * pow(2, u-1) + result == i1 + i2;
Dafny has some trouble with multiplication, as apparently multiplication is undecided-able, so it will likely not automatically verify. You will need to show inductively that your invariant is true, possibly requiring some lemmas about pow and your particular problem.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论