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

Question

您好，我认为在进行归纳时，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   ", i," r= ", 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,2,3,4]);
    print "\n";
    var sLc:nat := sumLeftChange([1,2,3,4]);
    print "\n";
    var sRc:nat := sumRightChange([1,2,3,4]);
    print "sl ", sl,"  sL= ",sLc, "\n";
    print "sr ", sr,"  sR= ",sRc, "\n";
}

Answer 1

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

这是一个例子，我们有一个真实的事实，即在你问它之前，Dafny 不会想自己“尝试”，但一旦你问它“嘿，是input[..i+1][..i] == input[..i]？”然后是说“哦，是的，很明显。”然后它有这个事实来帮助以后的证明。 （在 Dafny 中处理集合（例如集合、列表或映射）之间的方程式时，这种“你必须提出要求”的行为非常常见。有关更多信息，请参阅 this answer。）

---

可能更重要的问题是，我如何确定这是向 Dafny “指出”的正确事实？

方法如下。 （我很抱歉这花了多长时间，但我想向您展示我的完整过程并解释我在每个步骤中所做的事情。如果您不阅读全部内容，我不会被冒犯。）

我从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 + 1 替换所有出现的i。这是“相同的事实”，只是在不同的时间断言。由于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 == B、B == C 和C == D 来证明A == 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 语句正文的第二行，并且消息说“上一行和这行之间的计算步骤可能不成立”。基本上，达夫尼无法证明两条线相等。这并不奇怪，因为我们从一个失败的断言中生成了这个 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 同意我正在朝着正确的方向前进。

  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 不同意我们最近的简化。其次，Dafny 说我们新添加的行等于calc 语句的第一行！ （这里 Dafny 使用循环不变量的假设告诉我们r == sumSpecR(input[..i])。）所以即使我们从最后一行向上工作，我们现在实际上已经到达顶部，在第 2 行和第 3 行之间仍然存在间隙.

所以，Dafny 看不到这一点

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

我想给自己留个小纸条，提醒自己，如果没有这个断言，我认为证明将无法工作，同时我对为什么需要这个断言的最佳猜测也是如此。