Dafny语言中Product1乘法计算方法的循环不变量修正指导请求

Let's figure out where your current invariants are going wrong and fix them to make the method verify correctly. The core issue is that your invariants either don't hold at loop initialization, don't capture the actual progress of the loops, or are tautologies (statements that are always true and provide no useful information to the verifier).

Problems with Original Invariants #

• Outer Loop: Your first invariant res == m1*n + (m-m1)*n simplifies to res == m*n, which is only true when the loop finishes (not at the start, where res=0 and m1=0). This makes the verifier reject it immediately. The second invariant's equality is correct (res + (m-m1)*n == m*n), but it doesn't pair with a clear tracking of how res progresses with m1.
• Inner Loop: The invariants here are mostly tautologies. res + n == (res+n1 + (n-n1)) simplifies to res +n == res +n, which tells the verifier nothing about the actual state of the loop. You're not correctly tracking how res increases with each iteration of the inner loop.

Corrected Code with Proper Invariants #

method Product1 (m: nat, n: nat) returns (res:nat)
 ensures res == m * n; // Postcondition: result is m multiplied by n
{
 var m1: nat := 0;
 var n1: nat := 0;
 res := 0;
 while (m1 < m)
 // Invariant 1: res is the sum of m1 copies of n (so far, we've added n, m1 times)
 // Invariant 2: m1 never exceeds m, ensuring loop termination
 invariant res == m1 * n
 invariant m1 <= m
 {
 n1 := 0;
 while (n1 < n)
 // Invariant 1: res equals the sum of m1 copies of n plus n1 additional 1s
 // (we're in the process of adding the (m1+1)-th copy of n, one 1 at a time)
 // Invariant 2: n1 never exceeds n, ensuring inner loop termination
 invariant res == m1 * n + n1
 invariant n1 <= n
 {
 res := res + 1;
 n1 := n1 + 1;
 }
 // After inner loop: n1 == n, so res == m1*n +n = (m1+1)*n
 m1 := m1 + 1;
 }
 // After outer loop: m1 == m, so res == m*n (matches postcondition)
}

Explanation of the Fixed Invariants #

Let's walk through why these invariants work:

• Outer Loop Invariants:
  • res == m1 * n: This tracks the progress of the multiplication. m1 counts how many full groups of n we've added to res. When we start, m1=0 and res=0, so 0 == 0*n holds. Each iteration of the outer loop adds one full group of n (via the inner loop), then increments m1—so the invariant holds after each iteration.
  • m1 <= m: This ensures the outer loop will terminate, since m1 starts at 0 and increases by 1 each iteration until it reaches m.
• Inner Loop Invariants:
  • res == m1 * n + n1: This tracks the progress of adding the next group of n. When we start the inner loop, n1=0 and res is still m1*n (from the outer invariant), so res == m1*n +0 holds. Each iteration adds 1 to res and 1 to n1, so the equality remains true. When the inner loop finishes, n1=n, so res == m1*n +n = (m1+1)*n—which sets up the outer invariant for the next iteration.
  • n1 <= n: This ensures the inner loop terminates, as n1 starts at 0 and increments by 1 until it reaches n.

Finally, when the outer loop finishes, m1=m, so substituting into the outer invariant gives res == m*n, which exactly matches the postcondition. The verifier will now be able to prove the method is correct.

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