verification - 对 Dafny 后置条件消息感到困惑

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)    
   { 
    n1 := 0; 
    while (n1 < n)  
    { 
        res := res + 1;
        n1 := n1 + 1; 
    } 
    m1 := m1 + 1; 
    } 
}

当我用 dafny 验证它时，它说：

     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，但我无法弄清楚。