伪代码归纳证明

Question

我不太明白如何在伪代码上使用归纳证明。它的工作方式似乎与在数学方程上使用它的方式不同。

我正在尝试计算数组中可被 k 整除的整数的数量。

Algorithm: divisibleByK (a, k)
Input: array a of n size, number to be divisible by k
Output: number of numbers divisible by k

int count = 0;
for i <- 0 to n do
    if (check(a[i],k) = true)
        count = count + 1
return count;


Algorithm: Check (a[i], k)
Input: specific number in array a,  number to be divisible by k
Output: boolean of true or false

if(a[i] % k == 0) then
    return true;
else    
    return false;

如何证明这是正确的？谢谢

Answer 1

在这种情况下，我会将“归纳”解释为“迭代次数归纳”。

为此，我们首先建立一个所谓的循环不变。在这种情况下，循环不变式为：

           count 存储数字的数量可被 k 整除，且索引低于 i。

不变式保持循环入口，并确保在循环之后（当 i = n 时）count 保持可被 k 整除的值的数量整个数组。

归纳如下：

1. 基本情况：循环不变量在循环进入时成立（0 次迭代后）

   由于 i 等于 0，因此没有元素的索引低于 i。因此，索引小于 i 的元素都不能被 k 整除。 不变量成立。

2. 归纳假设：我们假设不变量在循环顶部成立。

3. 归纳步骤：我们证明了不变量在循环体的底部成立。

   执行主体后，i 已增加 1。为了使循环不变量在循环结束时保持不变，必须相应地调整 count。

   由于现在多了一个元素 (a[i])，其索引小于（新的）i，count如果（且仅当）a[i] 能被 k 整除时，应该加一，这正是 if 语句所确保的。

   因此循环不变量在循环体执行后也成立。

问。

---

在 Hoare-logic 中，它被证明（正式）如下（为了清楚起见，将其重写为 while 循环)：

{ I }
{ I[0 / i] }
i = 0
{ I }
while (i < n)
    { I ∧ i < n }
    if (check(a[i], k) = true)
        { I[i + 1 / i] ∧ check(a[i], k) = true }
        { I[i + 1 / i][count + 1 / count] }
        count = count + 1
        { I[i + 1 / i] }
    { I[i + 1 / i] }
    i = i + 1
    { I }
{ I ∧ i ≮ n }
{ count = ∑ 0 x < n;  1 if a[x] ∣ k, 0 otherwise. }

其中 I（不变量）为：

    count = Σ_{x <如果a[x]∣k，i} 1，否则为0。

（对于任何两个连续的断言行（{...}），都有一个证明义务（第一个断言必须暗示下一个断言），我将其作为练习留给读者；-）

Answer 2

我们通过对n（数组中元素的数量）进行归纳来证明正确性。你的范围是错误的，它应该是 0 到 n-1 或 1 到 n，但不是 0 到 n。我们假设 1 到 n。

在 n=0（基本情况）的情况下，我们只需手动执行算法即可。 counter 以值 0 启动，循环不会迭代，我们返回 counter 的值，正如我们所说，它是 0。这是正确的。

我们可以做第二个基本情况（尽管这是不必要的，就像常规数学一样）。 n=1。计数器初始化为 0。循环进行一次，其中 i 取值为 1，当且仅当 a 中的第一个值时，我们递增 counter > 可以被 k 整除（这是正确的，因为 Check 算法具有明显的正确性）。
因此，如果 a[1] 不能被 k 整除，我们返回 0，否则返回 1。这种情况也适用。

归纳起来很简单。我们假设 n-1 是正确的，并将证明 n（再次，就像常规数学一样）。为了更加正式，我们注意到 counter 保存了我们在循环中最后一次迭代结束时返回的正确值。

根据我们的假设，我们知道在 n-1 次迭代之后 counter 保存了数组中前 n-1 个值的正确值。我们调用 n=1 的基本情况来证明，当且仅当最后一个元素可被 k 整除时，它会在该值上加 1，因此最终值将是 n 的正确值。

量子ED。

您只需要知道对哪个变量执行归纳即可。通常输入大小是最有帮助的。另外，有时您需要假设所有小于 n 的自然数的正确性，有时只是 n-1。再次，就像常规数学一样。