10

我真的不明白如何通过对伪代码的归纳来证明。它似乎与在数学方程上使用它的方式不同。

我正在尝试计算数组中可被 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;

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

4

2 回答 2

14

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

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

             countk存储可被索引低于的数字的数量i。

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

归纳如下：

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

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

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

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

    在 body 被执行后，i被加一。为了使循环不变量在循环结束时保持不变，count必须进行相应的调整。

    由于现在还有一个元素 ( a[i]) 的索引小于 (new) i，count因此当（且仅当）a[i]可被 整除时，它应该加一k，这正是 if 语句所确保的。

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

Qed。

在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= ∑<sub>x < i 如果a[x]∣<em>k 为 1，否则为 0。

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

于 2011-10-08T21:00:37.703 回答
2

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

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

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

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

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

QED。

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

于 2011-10-08T21:00:23.640 回答