伪码的归纳证明

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.因此,由于count等于0,因此不变量成立.

2. 归纳假设:我们假设不变量保持在循环的顶部.

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

   身体执行后,i已经增加了一个.为了在循环结束时保持循环不变量,count必须相应地进行调整.

   由于现在还有一个元素(a[i])的索引小于(新的)i,count如果(并且只有)可a[i]被整除,则应该增加1 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=Σx _<i 1 if a[x]| k,否则为0.

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