Dafny整数乘法代码内层while循环的decreases值设置咨询

核心问题解答 #

内层循环正确的decreases值可以直接用b，这是最直观且易被Dafny验证的选择。

如果坚持想用b % 10，需要补充额外不变式帮助Dafny证明其合法性，但用b会更简洁高效。

代码中不变式与递减式的正确性分析 #

外层循环 #

• 不变式M * N == a * b + x：完全正确。它始终维护乘法等价关系：
  • 初始状态：a=N、b=M、x=0，等式M*N = N*M +0成立；
  • 内层循环执行时：x +=a、b -=1，代入等式得a*(b-1)+(x+a) = a*b -a +x +a = a*b +x，与原等式一致；
  • 外层循环更新时：a *=10、b := b/10，此时b是10的倍数（内层循环保证），设b=10k，则10a *k = a*10k =a*b，x不变，等式依然成立。
• 递减式b：正确。每次外层循环后b被除以10，严格递减且为自然数，最终会变为0，满足循环终止要求。

内层循环 #

• 原不变式M * N == a * b + x：正确，和外层循环逻辑一致，每次操作都能保持等式成立。
• 为什么用b%10会报错？
  Dafny需要严格证明递减式是非负且严格递减的自然数。虽然b%10在循环中确实递减（比如b=12→11，b%10从2→1），但Dafny无法自动推断其非负性和递减性，需要补充不变式：

  while (b % 10 != 0) 
    invariant M * N == a * b + x
    invariant b > 0  // 保证循环体内b为正，b%10非负
    decreases b % 10
  {
    x := x + a; 
    b := b - 1;
  }
  

  但直接用b作为decreases值无需额外不变式，Dafny能直接验证b在每次循环中严格递减，且不会破坏外层循环的递减逻辑。

修正后的完整代码 #

method MultiplyTheory(N: int, M: nat) returns (Res: int)
  ensures Res == M*N;
  requires N>=0 && M>=0;
{
  var a := N;
  var b := M;
  var x := 0;
  var i :=0;
  while (b > 0)    
  invariant M * N == a * b + x
  decreases b
  {
    while (b % 10 != 0) 
    invariant M * N == a * b + x    
    decreases b  // 使用b作为递减值
    {
      x := x + a; 
      b := b - 1;
      
    }
    a := 10 * a;
    b := b / 10; 
  
  }
  Res := x; 
}

内容的提问来源于stack exchange，提问作者Engr Aminul Islam