Dafny代码中后置条件存在的问题排查——BP5003报错分析

Problem Analysis #

The BP5003 error happens because your loop invariant is too weak to let Dafny connect the loop's behavior to the postcondition. The existing invariant only tracks the range of i, but it doesn't describe how the array elements are being transformed to match the sumTo-based requirement.

Your prod method is intended to compute the suffix sum of the array (each element t[k] becomes the sum of old(t)[k] through old(t)[t.Length-1]), but Dafny can't infer the relationship between the loop's modifications and the sumTo function without explicit, state-tracking invariants.

Solution: Strengthen the Loop Invariants #

To fix this, you need to add invariants that explicitly track which parts of the array already satisfy the postcondition, and how the current state relates to the original array (old(t)). Here's the corrected code with explanations:

function sumTo(a: array<int>, k: int, j: int): int 
  requires a != null; 
  requires 0 <= k && k <= a.Length; 
  requires k <= j && j <= a.Length - 1; 
  decreases j; 
  reads a; 
{ 
  if (k == j) then a[k] else sumTo(a, k, j-1) + a[j] 
} 

method prod(t: array<int>) 
  modifies t 
  requires t != null && t.Length >= 2 
  ensures forall k: int :: 0 <= k < t.Length ==> t[k] == sumTo(old(t), k, t.Length - 1) 
{ 
  var i := t.Length - 2; 
  while i >= 0 
    // Original invariant: track the range of i
    invariant t.Length - 1 > i >= -1; 
    // All positions after i+1 already hold the correct suffix sum
    invariant forall m: int :: i+1 < m < t.Length ==> t[m] == sumTo(old(t), m, t.Length - 1);
    // The position i+1 holds the correct suffix sum (critical for updating t[i])
    invariant t[i+1] == sumTo(old(t), i+1, t.Length - 1);
    decreases i; 
  { 
    t[i] := t[i] + t[i+1]; 
    i := i - 1; 
  } 
}

Key Explanations: #

• First new invariant: This tells Dafny that every position m greater than i+1 already matches the postcondition (it's the sum of the original array from m to the end). This holds initially when i = t.Length-2 (since there are no positions greater than i+1 = t.Length-1), and is preserved through each iteration.
• Second new invariant: This guarantees that the position immediately after i (i+1) has the correct suffix sum. When we update t[i] to t[i] + t[i+1], this transforms t[i] from the original old(t)[i] to old(t)[i] + sumTo(old(t), i+1, t.Length-1)—which is exactly sumTo(old(t), i, t.Length-1) (by the definition of sumTo).
• Loop termination: When i = -1, the invariants imply that all positions m >= 0 (since i+1 = 0) satisfy the postcondition, which directly matches the ensures clause.

Additional Notes #

If Dafny still struggles with verifying the sumTo function's properties, you could add a helper lemma to formally prove that sumTo(a, k, j) = sumTo(a, k, j-1) + a[j] for k < j—though in this case, the function's recursive definition should already make this relationship obvious to Dafny's verifier.

内容的提问来源于stack exchange，提问作者Shapagat Bolat