伪代码的归纳证明

Question

给出伪代码

MUL(a,b) 
   x=a
   y=0
   WHILE x>=b DO
      x=x-b
      y=y+1
   IF x=0 THEN
      RETURN(true)
   ELSE
      RETURN(false)

令x(n)和y(n)表示while循环运行 n次后x和y的值。

我必须通过归纳法证明

x(n) + b*y(n) = a

我做了什么：

P(n): x(n) + by(n) = a

设 a 和 b 为任意数，那么第一个循环将给出 x(1) = a - b 和 y(1) = 0 + 1 = 1

P(1): x(1) + by(1) = a <=> a = a

所以 P(1) 为真。

假设 P(n) 为真。我们想证明 P(n+1) 也是真的。

对于第 n + 1 步，循环将给出 x(n+1) = x(n) - b 和 y(n+1) = y(n) + 1

P(n+1): x(n+1) + by(n+1) = a <=> x(n) + by(n) = a

假设P(n)为真，则P(n+1)也为真，证明完成

我的问题： 由于这是我第一次在伪代码上使用归纳证明，所以我不确定如何去做。我只想知道这是否是解决问题的正确方法，如果不是，流程应该是什么样的？

谢谢

Answer 1

因为你的问题（几乎）是正确的，所以回答这个问题感觉有点矫枉过正，但我​​还是会这样做：

你的方法很好，尽管你不应该忽略根本没有执行循环迭代的情况，这种情况是 a < b 并且对应于 P₀。如果证明P₁为真，且P_n+1[=当P_n为真时77=]为真，你什么都不说P₀ .

所以稍微修改一下，通过归纳法推导证明如下：

定义P_n作为n[=77=后表达式x + b*y的值] 循环迭代已执行：

P_n : x_n + b.y_n = a

需证明P_n对所有n >= 0[=77=成立]

1。基本情况：P₀

请注意，这是一种可能的情况：当第一次评估 while 循环的条件时，尚未执行任何迭代，因此 n 为 0，但我们确实有两个变量的值在起作用：x₀ 和 y₀。

循环的前置条件由循环之前的赋值语句决定：

x=a
y=0

所以我们有：

P₀ : x₀ + b.y₀ = a + b.0 = a

2。归纳步长：P_n+1

这里我们假设 P_n 对于给定的 n 为真:

P_n : x_n + b.y_n = a

这是开始下一次循环迭代时的前置条件，其中执行以下语句：

x=x-b
y=y+1

通过替换，我们得到了特定迭代的 post-条件，根据定义，它是 P_n+1:

P_n+1 : (x_n - b) + b.(y_n + 1) = x_n + b.y_n = P_n = a