证明通过诱导伪code [英] Proof by Induction of Pseudo Code
问题描述
我真的不知道如何人使用的证明用归纳法的伪code。它似乎并没有以同样的方式工作作为使用它的数学方程式。
I don't really understand how one uses proof by induction on psuedocode. It doesn't seem to work the same way as using it on mathematical equations.
我想算的整型整除K的数组的数量。
I'm trying to count the number of integers that are divisible by k in an array.
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;
将如何证明这是正确的吗？谢谢
How would one prove that this is correct? Thanks
推荐答案
在这种情况下，我会除preT感应作为诱导了迭代的次数。
In this case I would interpret "inductively" as "induction over the number of iterations".
要做到这一点，我们首先建立一个所谓的循环不变。在这种情况下，循环不变是：
To do this we first establish a so called loop-invariant. In this case the loop invariant is:
<$c$c>count门店数整除的数除以 K 比指数下我。
count stores the number of numbers divisible by k with index lower than i.
这个不变式在循环入口，并确保以后的循环（当 I = N ）计数持有价值整除的数除以 K 中的全部的数组。
This invariant holds upon loop-entry, and ensures that after the loop (when i = n) count holds the number of values divisible by k in whole array.
感应看起来是这样的：
-
基本情况：循环不变式在循环入口（后0迭代）
Base case: The loop invariant holds upon loop entry (after 0 iterations)
由于我等于0，没有元素比指数下我。因此，没有比指数更少的I 元素整除 K 。因此，由于计数等于0的不变式。
Since i equals 0, no elements have index lower than i. Therefore no elements with index less than i are divisible by k. Thus, since count equals 0 the invariant holds.
归纳假设：我们假定不变式的的的圈顶部的
Induction hypothesis: We assume that the invariant holds at the top of the loop.
归纳步：我们表明，保持不变的的循环体的底部的
Inductive step: We show that the invariant holds at the bottom of the loop body.
在我已加一。对于循环不变保持在循环结束时，计数必须作相应的调整。
After the body has been executed, i has been incremented by one. For the loop invariant to hold at the end of the loop, count must have been adjusted accordingly.
由于现在多了一个元素（ A [1] ）其中有一个指标小于（新）我，计数应该已经增加了一个，如果（且仅当） A [1] 是整除 K ，这是precisely什么if语句保证。
Since there is now one more element (a[i]) which has an index less than (the new) i, count should have been incremented by one if (and only if) a[i] is divisible by k, which is precisely what the if-statement ensures.
于是的循环不变还保持着身体已经执行后。
Thus the loop invariant holds also after the body has been executed.
QED。
在霍尔逻辑它的证明（正式）这样的（重写它作为一个在─回路清晰度）：
In Hoare-logic it's proved (formally) like this (rewriting it as a while-loop for clarity):
{ 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. }
其中，我（不变）是：
＆NBSP;＆NBSP;＆NBSP;＆NBSP;＆NBSP; 计数 =Σ<子系列> X＆LT;我 1，如果 A [X] | K 的，否则为0
count = ∑x < i 1 if a[x]∣k, 0 otherwise.
（对于两个连续的断言行（ {...} ）有一个证明的义务（第一个断言一定意味着在未来），我保留为一个练习为读者; - ）
(For any two consecutive assertion lines ({...}) there is a proof-obligation (first assertion must imply the next) which I leave as an exercise for the reader ;-)
这篇关于证明通过诱导伪code的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
