求Dafny中两整数乘法程序的循环不变式与递减表达式

这个方法通过将M分解为15的倍数组合实现乘法，核心逻辑是维护x + a*b始终等于目标乘积N*M——所有循环操作都是等价变换，不会改变这个总和。以下是两个循环的不变式与递减表达式分析：

外层循环（while (b > 0)） #

循环不变式（invariant） #

invariant x + a * b == N * M
invariant a >= 0 && b >= 0 && x >= 0

• 第一个不变式是核心约束：初始状态x=0、a=N、b=M时满足0 + N*M = N*M；内层循环执行后等式保持成立，外层循环的a:=15*a; b:=b/15操作也等价于a*b值不变（当b是15的倍数时，15a*(b/15) = a*b），因此整个外层循环过程中该等式始终成立。
• 第二个不变式约束变量范围：保证a、b、x均为非负整数，符合前置条件N>=0、M>=0的推导。

递减表达式（decreases） #

decreases b

进入循环时b>0，每次循环b会被15取整除法，结果必然严格小于原b，且b是nat类型，最终会递减到0，满足Dafny的终止性要求。

内层循环（while (b % 15 != 0)） #

循环不变式（invariant） #

invariant x + a * b == N * M
invariant a >= 0 && b > 0 && x >= 0

• 核心不变式同样为x + a*b == N*M：每次循环执行x +=a、b -=1，等价于(x+a) + a*(b-1) = x +a +a*b -a = x+a*b，总和完全不变，等式始终成立。
• 变量范围约束：b>0由外层循环条件b>0和内层循环条件b%15!=0保证（此时b至少为1）；a和x的非负性由初始值和操作逻辑维持。

递减表达式（decreases） #

decreases b

内层循环每次执行b -=1，b为正整数且严格递减，直到b%15==0时退出循环，满足终止性要求。

完整可验证代码 #

method MultiplyTwoNumber(N: int, M: nat) returns (Result: int)
  ensures Result == M*N;
  requires N>=0 && M>=0;
{
  var a := N;
  var b := M;
  var x := 0;
  var i :=0;
  while (b > 0)    
  invariant x + a * b == N * M
  invariant a >= 0 && b >= 0 && x >= 0
  decreases b
  {
    while (b % 15 != 0)   
    invariant x + a * b == N * M
    invariant a >= 0 && b > 0 && x >= 0
    decreases b
    {
      x := x + a; 
      b := b - 1; 
      
    }
    a := 15 * a; 
    b := b / 15; 
  
  }
  Result := x; 
}

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