Dafny可以从右边验证求和元素吗？

问题描述

嗨，我发现执行归纳Dafny时会展开功能说明。因此，在编写实现该功能的方法时，最好以相似的方向遍历数组。这种理解对应于 sumLeftChange（如下所示），但我根本无法验证sumRightChange。谁能解释我所缺少的吗？

function method sumSpec(input:seq<nat>) : nat
decreases input 
{  if |input| == 0 then 0 else input[0]+ sumSpec(input[1..]) }
function method sumSpecR(input:seq<nat>) : nat
decreases input 
{ if |input| == 0 then 0 else input[|input|-1]+ sumSpecR(input[..|input|-1]) }
method sumLeftChange(input:seq<nat>) returns (r:nat)
  ensures r == sumSpec(input)
//  ensures r == sumSpecR(input)
{   r :=0; var i:nat := 0;
    while (i<|input|)
     decreases |input| - i
     invariant i<= |input|
     invariant  r == sumSpec(input[|input| - i..])
   //  invariant  r == sumSpecR(input[|input| - i..]) //fails and should fail
    {   r:= r+input[|input| - i-1]; // first element is from right |input|-1
        i := i+1;
        print "sumLeftChange  ",i," r  ",r,"  ",sumSpec(input[|input| - i..]),"\n";
    } 
}
method sumRightChange(input:seq<nat>) returns (r:nat)
{  r :=0; var i:nat := 0;
    while (i<|input|)
     decreases |input| - i
     invariant i <= |input|    
    // invariant  r == sumSpecR(input[..i]) //I can get nothing to work
    {  
        r:= r+input[i];  // first element is from left  0     
        i := i+1; 
    print "sumRightChange   "," r= ","  sumSpecR(input[..i])= ",sumSpecR(input[..i]),"\n";
    }
}
method Main() {
    var sl:nat := sumSpec([1,2,3,4]);
    print "\n";
    var sr:nat := sumSpecR([1,4]);
    print "\n";
    var sLc:nat := sumLeftChange([1,4]);
    print "\n";
    var sRc:nat := sumRightChange([1,4]);
    print "sl ",sl,"  sL= ",sLc,"\n";
    print "sr ",sr,"  sR= ",sRc,"\n";
}

解决方法

在循环主体的开头添加assert input[..i+1][..i] == input[..i];将导致sumRightChange进行验证。

在这种情况下，我们有一个真实的事实，那就是达芙妮在您提出要求之前不会考虑自己“尝试”，而是一旦您提出要求，“ input[..i+1][..i] == input[..i]是吗？”然后说：“哦，是的，显然。”然后它具有一个事实，可以在以后帮助证明。（在Dafny中使用集合，集合或列表之类的集合之间的方程式时，这种“必须要求”的行为非常普遍。有关更多信息，请参见this answer。）

也许更重要的问题是，我如何确定这是“指出”达夫尼的正确事实？

这是怎么回事。（很抱歉，我花了多长时间，但是我想向您展示我的完整流程，并解释我在每个步骤中所做的事情。如果您不全部阅读，我不会感到冒犯。）

我从sumRightChange内部的以下循环开始，取消了对失败的不变式的注释。（为简洁起见，我删除了print语句。）

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {
    r := r + input[i]; 
    i := i + 1;
  }

Dafny报告“可能无法保持不变”。我知道这意味着Dafny试图在循环的底部声明不变量，但失败了。为了仔细检查自己，我复制粘贴了不变式并将其转换为循环底部的断言。

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {
    r := r + input[i]; 
    i := i + 1;
    assert r == sumSpecR(input[..i]);  // added this line
  }

正如预期的那样，Dafny报告违反声明。但是，不变式上的错误消失了，这使我充满信心，只要我能证明这个断言，我就完成了。

我也知道我要假设循环顶部是不变的。我想将这两个事实（顶部假定的不变性和底部确定的不变性）相互“移动”。事实证明，向后移动比向前移动要容易，所以我将尝试一点一点地将循环底部的断言向上移动。

在断言中向后移动断言的技巧是在断言中手动“撤消”该断言。因此，为了在断言r == sumSpecR(input[..i])上向后移动断言i := i + 1，我将用i替换所有i + 1的出现。这是在不同时间断言的“相同事实”。由于i的值在不同的时间是不同的，因此必须对声明进行语法修改以使其成为“相同事实”。希望这是有道理的...无论如何，执行该转换会产生此循环：

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {
    r := r + input[i];
    assert r == sumSpecR(input[..i+1]);  // moved this assertion up one line
    i := i + 1;
  }

Dafny仍报告断言冲突。而且严格仍然不报告不变的违规。因此，我们仍然知道，如果可以证明断言，就可以验证整个循环。

（请注意，如果我们在移动断言时出错，将会发生什么情况。例如，如果我们没有将i手动替换为i+1，而是仅仅将断言向上移动了一行，那么会发生什么。 Dafny报告了一个断言冲突和一个不变的冲突，所以我们知道我们搞砸了！）

现在让我们在断言r := r + input[i];上向后再移一行断言。同样，技巧是通过在断言中将r替换为r + input[i]来手动撤消此分配，如下所示：

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {  
    assert r + input[i] == sumSpecR(input[..i+1]);  // moved this assertion up one line
    r := r + input[i];
    i := i + 1;
  }

再次，Dafny报告了一个断言冲突，但没有一个不变的冲突。（同样，如果我们搞砸了，它会报告一个不变的违规。）

现在，我们在循环的顶部有了断言，我们知道不变式成立。是时候做个证明了。

我们正试图证明一个方程。我喜欢使用Dafny的calc语句调试有关方程式的证明。如果您不熟悉calc语句，则基本格式为

calc {
  A;
  B;
  C;
  D;
}

通过证明A == D，A == B和B == C来证明C == D。这提供了一种方便的方法，可以在方程证明中添加中间步骤，并缩小Dafny混淆的确切范围。

要将方程的断言转换为calc语句，我们只需将方程的左手放在第一行，而将右手放在第二行。到目前为止，这没有任何改变，但我们只需确保：

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {
    // replaced old assertion with the following calc statement
    calc {
      r + input[i];
      sumSpecR(input[..i+1]);
    }
    r := r + input[i];
    i := i + 1;
  }

Dafny在calc语句中报告了一个错误，但是在invariant上却没有，因此我们仍然知道我们已经证明了正确的事实，可以完成对循环的验证。

该错误位于calc语句主体的第二行，并且消息显示“上一行与此行之间的计算步骤可能不成立”。基本上，Dafny无法证明两条线相等。不足为奇，因为我们是根据失败的断言产生的calc语句。

现在，我们可以开始添加中间步骤了。有时，从最上面的行开始工作是有意义的，而其他时候，从最后一行开始行是有意义的。我认为第二种策略在这里更有意义。

让我们手动展开sumSpecR的定义，看看我们遇到的困难。查看sumSpecR的定义，首先检查是否为|input| == 0。请注意，因为input是指sumSpecR的自变量，而不是sumRightChange的自变量！在我们的calc语句的最后一行的上下文中，我们将input[..i+1]传递到sumSpecR中，因此定义正在询问此列表的长度是否为零。但是我们知道它不是，因为i >= 0加上1。因此，我们将进入定义的else分支。

else分支从右边分开列表。让我们尝试系统一点，只复制粘贴定义的else分支，用实际参数input[..i+1]代替参数名称input。（我喜欢使用文本编辑器搜索并替换此步骤。）

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {  
    calc {
      r + input[i];
      // added the following line by copy-pasting the else branch of the 
      // definition of sumSpecR and then replacing its parameter
      // input with the actual argument input[..i+1]
      input[..i+1][|input[..i+1]|-1] + sumSpecR(input[..i+1][..|input[..i+1]|-1]);
      sumSpecR(input[..i+1]);
    }
    r := r + input[i];
    i := i + 1;
  }

现在，请密切注意错误消息会发生什么。它向上移动！这意味着我们正在取得进步，因为Dafny同意我们的观点，calc语句主体的新中间线等于最后一行。

我们现在可以做很多简化。让我们首先将|input[..i+1]|简化为i+1。您可以通过修改我们刚刚添加的行来做到这一点，但是我想通过在其上方添加另一行来做到这一点，这样我就可以记录我的进度，并确保Dafny同意我朝着正确的方向前进。 / p>

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {  
    calc {
      r + input[i];
      // added the following line simplifying |input[..i+1]| into i+1
      input[..i+1][i+1-1] + sumSpecR(input[..i+1][..i+1-1]);
      input[..i+1][|input[..i+1]|-1] + sumSpecR(input[..i+1][..|input[..i+1]|-1]);
      sumSpecR(input[..i+1]);
    }
    r := r + input[i];
    i := i + 1;
  }

同样，错误消息上移一行。是的！

现在，我们可以将i+1-1简化为i，也可以将input[..i+1][i]简化为input[i]。同样，我更喜欢在新行中进行此操作。

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {  
    calc {
      r + input[i];
      input[i] + sumSpecR(input[..i+1][..i]);  // added this line
      input[..i+1][i+1-1] + sumSpecR(input[..i+1][..i+1-1]);
      input[..i+1][|input[..i+1]|-1] + sumSpecR(input[..i+1][..|input[..i+1]|-1]);
      sumSpecR(input[..i+1]);
    }
    r := r + input[i];
    i := i + 1;
  }

错误消息继续前进。

我想做的下一个简化是将input[..i+1][..i]转换为input[..i]。再次，我使用换行符。

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {  
    calc {
      r + input[i];
      input[i] + sumSpecR(input[..i]);  // added this line
      input[i] + sumSpecR(input[..i+1][..i]);
      input[..i+1][i+1-1] + sumSpecR(input[..i+1][..i+1-1]);
      input[..i+1][|input[..i+1]|-1] + sumSpecR(input[..i+1][..|input[..i+1]|-1]);
      sumSpecR(input[..i+1]);
    }
    r := r + input[i];
    i := i + 1;
  }

请密切注意错误消息的发生情况。它不动！这告诉我们两件事。首先，达夫尼不同意我们最近的简化。第二，Dafny说，我们新添加的行等于calc语句的第一行！（此处，Dafny利用循环不变的假设告诉我们r == sumSpecR(input[..i])。）因此，即使我们从最后一行开始进行工作，但实际上我们已经到达顶部，而第2行之间仍然留有间隙和3。

所以，达夫妮没看到

input[i] + sumSpecR(input[..i]) == input[i] + sumSpecR(input[..i+1][..i])

有什么作用？表达式input[i]出现在两侧，因此剩下要显示的是

sumSpecR(input[..i]) == sumSpecR(input[..i+1][..i])

在这里，我们有一个函数sumSpecR应用于两个我们认为相同的语法不同的参数。此时sumSpecR的定义无关紧要，重要的是它是一个应用于相等参数的函数。因此，我们可以尝试检查参数是否确实相等。

assert input[..i] == input[..i+1][..i];

这就是我们需要获得完整证明才能通过的断言。

在这样的调试过程结束时，我通常喜欢清理并仅保留Dafny实际需要进行证明的事实。因此，我只是尝试删除内容并查看证明是否仍然有效。在这种情况下，只需要我们发现的最后一个断言即可；其他所有内容都可以删除。

这是我的最后一个循环：

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {
    assert input[..i] == input[..i+1][..i];  // load-bearing assertion due to sequence extensionality
    r := r + input[i];
    i := i + 1;
  }

我想给自己留下一点笔记，以提醒我，如果没有此断言以及我对为什么需要断言的最佳猜测，我认为该证明将不起作用。

dafny induction loops

Dafny可以从右边验证求和元素吗？

问题描述

解决方法

相关问答