我不太明白如何在伪代码上使用归纳证明。它的工作方式似乎与在数学方程上使用它的方式不同。
我正在尝试计算数组中可被 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;
如何证明这是正确的？谢谢
在这种情况下，我会将“归纳”解释为“迭代次数归纳”。
为此，我们首先建立一个所谓的循环不变 http://en.wikipedia.org/wiki/Loop_invariant。在这种情况下，循环不变量是：
count存储可被整除的数字个数k指数低于i.
这个不变量在循环进入时保持不变，并确保在循环之后（当i = n) count保存可被整除的值的数量k in whole array.
归纳如下：
-
基本情况：循环不变量在循环进入时成立（0 次迭代后）
Since i等于 0，没有元素的索引低于i。因此没有索引小于的元素i可以被整除k。因此，自从count等于 0 不变式成立。
归纳假说：我们假设不变量保持在循环顶部.
-
感应步骤：我们证明不变量在循环体的底部.
尸体被处决后，i已增加一。为了使循环不变量在循环结束时保持不变，count必须进行相应的调整。
由于现在多了一个元素 (a[i]) 其索引小于（新的）i, count当（且仅当）时应该加一a[i]可以整除k，这正是 if 语句所确保的。
Thus循环不变量在循环体执行后也保持不变。
Qed.
In 霍尔逻辑 http://en.wikipedia.org/wiki/Hoare_triple它被（正式）证明如下（为了清楚起见，将其重写为 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. }
Where I（不变量）是：
count = ∑x < i 1 if a[x]∣k, 0 otherwise.
（对于任意两个连续的断言行（{...}）有一个证明义务（第一个断言必须暗示下一个断言），我将其作为练习留给读者;-)
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
