Dafny后置条件消息引起困惑 [英] Confused by Dafny postcondition messages

查看:192
本文介绍了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屋!

查看全文
登录 关闭
扫码关注1秒登录
发送“验证码”获取 | 15天全站免登陆