伪码的归纳证明

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存储索引低于i的k可整除的数的个数。

这个不变量在循环进入时成立，并确保在循环之后(当i = n) count保存整个数组中可被k整除的值的个数。

归纳如下:

1. 基本情况:循环不变量在循环进入(0次迭代后)时保持

   由于i = 0，所以没有元素的索引值低于i。因此索引小于i的元素不能被k整除。因此，由于count = 0，该不变式成立。

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

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

   体执行后，i加1。要使循环不变式在循环结束时保持不变，必须对count进行相应的调整。

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

   因此循环不变式在程序体执行后仍然有效。

Qed .

---

在Hoare-logic中(形式上)是这样证明的(为了清晰起见，将其重写为while-loop):

{ 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中的第一个值能被k整除，则对counter加1(由于Check算法的明显正确性，这是正确的)。
因此，如果a[1]不能被k整除，则返回0，否则返回1。

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

根据我们的假设，我们知道经过n-1次迭代后，counter对于数组中的前n-1个值保持正确的值。我们调用n=1的基本情况来证明，如果最后一个元素能被k整除，它将在这个值上加1，因此最终值将是n的正确值。

QED .

你只需要知道在哪个变量上执行归纳。通常输入的大小是最有帮助的。而且，有时候你需要假设所有小于n的自然数都是正确的，有时候只有n-1。和普通数学一样