Dafny后置条件消息引起困惑 [英] Confused by Dafny postcondition messages
本文介绍了Dafny后置条件消息引起困惑的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!
问题描述
一个非常简单的乘法代码:
A very simple multiplication code:
method Product1 (m: nat, n: nat) returns (res:nat)
ensures res == m * n;
{
var m1: nat := 0;
var n1: nat := 0;
res := 0;
while (m1 < m)
{
n1 := 0;
while (n1 < n)
{
res := res + 1;
n1 := n1 + 1;
}
m1 := m1 + 1;
}
}
当我与dafny验证时,它说:
When I verify it with dafny, it says:
Description Line Column
1 A postcondition might not hold on this return path. 8 4
2 This is the postcondition that might not hold. 2 16
在某些条件下,我得到说,res!= m * n,但我可以
I get it says under some conditions, res != m*n, but I can't figure it out.
推荐答案
已更新!
尝试了dafny 在线网站,看起来像是虫子?
Tried dafny in the online website, looks like it is bug?
method Test(m: nat) returns (r: nat)
{
var m1: nat := 0;
while (m1 < m) {
m1 := m1 + 1;
}
assert m == m1; // fail assert
}
更多尝试:
method Test(m: nat) returns (r: nat)
{
var m1: nat := 0;
while (m1 < m) {
assert m1 < m;
m1 := m1 + 1;
}
assert !(m1 < m); // pass
assert m1 == m || m1 > m; // pass
assert m1 == m; // fail
}
深入了解之后,我知道应该使用 Loop Invariants
来解决这个问题。
After some deep understand, I know that it should use Loop Invariants
for dafny to address this question.
我的修改代码:
method Product1 (m: nat, n: nat) returns (res:nat)
ensures res == m * n;
{
var m1: nat := 0;
var n1: nat := 0;
res := 0;
while (m1 < m)
invariant 0 <= m1 <= m
invariant res == m1 * n
{
var temp: nat := res;
n1 := 0;
while (n1 < n)
invariant 0 <= n1 <= n
invariant res == temp+n1
{
res := res + 1;
n1 := n1 + 1;
}
m1 := m1 + 1;
}
assert m1 == m; // success
}
然后删除tmp var:
Then remove the tmp var:
method Product1 (m: nat, n: nat) returns (res:nat)
ensures res == m * n;
{
var m1: nat := 0;
var n1: nat := 0;
res := 0;
while (m1 < m)
invariant 0 <= m1 <= m
invariant res == m1 * n
{
n1 := 0;
while (n1 < n)
invariant 0 <= n1 <= n
invariant res == n1 + m1*n
{
res := res + 1;
n1 := n1 + 1;
}
m1 := m1 + 1;
}
assert m1 == m; // success
}
这篇关于Dafny后置条件消息引起困惑的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!
查看全文