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

この場合、「帰納的に」を「反復回数にわたる帰納」と解釈します。

これを行うには、最初にいわゆるloop-invariantを確立します。この場合、ループ不変条件は次のとおりです。

             countkより小さいインデックスで割り切れる数の数を格納しますi。

この不変条件は、ループの入り口で保持され、ループの後 ( when i = n)が配列全体でcount割り切れる値の数を保持することを保証します。k

誘導は次のようになります。

  1. 基本ケース: ループ不変式はループ エントリで保持されます (0 回の反復後)

    は 0 に等しいためi、 より小さいインデックスを持つ要素はありませんi。したがって、 より小さいインデックスを持つ要素iは で割り切れませんk。したがって、countは 0 に等しいので、不変式が成り立ちます。

  2. 帰納仮説:ループの先頭で不変条件が成り立つと仮定します。

  3. 帰納的ステップ:ループ本体の底で不変条件が成り立つことを示します。

    本体が実行された後、i1 ずつインクリメントされています。ループの最後で保持されるループ不変条件については、countそれに応じて調整されている必要があります。

    a[i](新しい) よりも小さいインデックスを持つ要素 ( ) がもう 1 つあるためi、が で割り切れるcount場合 (およびその場合にのみ) は 1 ずつインクリメントされるべきであり、これはまさに if ステートメントによって保証されます。a[i]k

    したがって、本体が実行された後もループ不変条件が保持されます。

Qed。

Hoare ロジックでは、(形式的に) 次のように証明されています (明確にするために 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。

(任意の 2 つの連続するアサーション行 ( {...}) には、証明義務 (最初のアサーションは次のアサーションを含意する必要があります) があります。これは、読者の演習として残しておきます ;-)

于 2011-10-08T21:00:37.703 に答える
2

n配列の要素数 の帰納法によって正しさを証明します。範囲が間違っています。0 から n-1 または 1 から n のいずれかである必要がありますが、0 から n ではありません。1 ～ n と仮定します。

n=0 の場合 (基本ケース)、単純にアルゴリズムを手動で実行します。はcounter値 0 で開始され、ループは繰り返されず、counter の値が返されますが、前述のように 0 でした。これは正しいです。

2 番目の基本ケースを実行できます (ただし、通常の数学と同様に不要です)。n=1。カウンターは 0 で初期化されます。ループは 1 つのパスを作成し、i値 1 を取りcounter、最初の値aが割り切れる場合にインクリメントします (アルゴリズムkが明らかに正しいため、これは正しいです)。 したがって、が で割り切れない場合は0 を返し、そうでない場合は 1 を返します。この場合も同様です。Check
a[1]k

誘導は簡単です。n-1 の正しさを仮定し、n について証明します (繰り返しますが、通常の数学と同じように)。適切に形式化するために、 は loop の最後の反復の終わりまでにcounter返す正しい値を保持していることに注意してください。

私たちの仮定により、n-1回の反復の後counter、配列の最初のn-1個の値に関して正しい値が保持されることがわかります。n=1 の基本ケースを呼び出して、最後の要素が k で割り切れる場合、この値に 1 が追加されることを証明します。したがって、最終的な値は n の正しい値になります。

QED。

誘導を実行する変数を知る必要があるだけです。通常、入力サイズが最も役立ちます。また、n 未満のすべての自然数、場合によっては n-1 だけが正しいと仮定する必要がある場合もあります。繰り返しますが、通常の数学と同じように。

于 2011-10-08T21:00:23.640 に答える