用于证明三数最大值程序终止性的递减变体函数求解

给定的Hoare三元组 #

{ X ≥ 0 ∧ Y ≥ 0 ∧ Z ≥ 0 }
  x, y, z := X, Y, Z; 
  m := 0;
  do   x > m → m := x
    ⌷  y > m → m := y
    ⌷  z > m → m := z
  od
{ m = max(X, Y, Z) ∧ x = X ∧ y = Y ∧ z = Z ∧ X ≥ 0 ∧ Y ≥ 0 ∧ Z ≥ 0 }

递减变体函数的选择 #

你提到的函数 max(X, Y, Z) − m 完全可以作为证明该程序终止的递减变体函数，验证如下：

• 非负性：初始时m=0，结合前置条件中X,Y,Z均非负，max(X,Y,Z)≥0，因此初始值max(X,Y,Z)-0 = max(X,Y,Z) ≥0；每次循环仅在x/y/z > m时执行赋值，新的m严格大于旧值，但m始终不会超过max(X,Y,Z)，因此max(X,Y,Z)-m始终非负。
• 严格递减性：每次循环执行任意分支后，m都会被更新为更大的数值，因此max(X,Y,Z)-m会严格减小。
• 终止触发：当max(X,Y,Z)-m = 0时，m = max(X,Y,Z)，此时循环的三个分支条件x>m、y>m、z>m均不成立（因为x=X≤max(X,Y,Z)=m，y=Y≤m，z=Z≤m），循环终止。

内容的提问来源于stack exchange，提问作者ARMAN 阿尔曼