Dafny事後条件メッセージ

Question

A非常に単純な乗算コードで混乱：

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 =メートル下に！ * nしかし、私はそれを把握することはできません。

Answer 1

更新済み！

online websiteで試したダフィー、はバグのようですか？

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 
} 

一部は深く理解した後、私はそれがこの質問に対処するためにdafnyためLoop Invariantsを使用する必要があることを知っています。

私の修正コード：

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削除：

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 
} 

Answer 2

あなたのループは、任意のループ不変条件を表示できません。少なくとも、両方のループで不変量が必要です。それ以外の場合、Dafnyはループの後に保持されているものを把握することができません...