# 对Dafny的后置条件信息感到困惑[英] Confused by Dafny postcondition messages

### 问题描述

```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;
}
}
```

```    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
```

## 推荐答案

```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
}
```

```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
}
```

```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
}
```