Dokazivanje korektnosti algoritma

Definicija: Invarijanta petlje je relacija izmedju promenljivih koja važi nakon svakog izvršenja bloka naredbi u okviru petlje.

Zadaci

Zadatak 1

Napisati algoritam za odredjivanje najvećeg zajedničkog delioca dva prirodna broja i dokazati korektnost napisanog algoritma.

Rešenje: Euklidov algoritam se bazira na sledećem tvrdjenju:

Tvrdjenje: NZD(a, b) = NZD(b, r), pri čemu je r = a % b.

Na osnovu ovog tvrdjenja imamo naredni pseudokod algoritma:

    nzd(m, n) {
        a = max(m, n);
        b = min(m, n);

        r = b;

        while (r > 0) {
            r = a % b;
            a = b;
            b = r;
        }

        return a;
    }

Pokažimo ispravnost ovog algoritma.

Uočimo svojstvo nzd(m, n) = nzd(a, b) kao invarijantu petlje. Pokažimo indukcijom da ovo tvrdjenje važi.

Baza: pre ulaska u petlju tvrdjenje važi jer važi:

nzd(a, b) = nzd(max(m, n), min(m, n)) = nzd(m, n)

Induktivni korak: Pretpostavimo da tvrdjenje nzd(a, b) = nzd(m, n) važi pre nekog izvršenja bloka naredbi u okviru petlje i pokažimo da važi i nakon toga.

Nakon narednog izvršenja bloka menjaju se vrednosti promenljivih a i b na sledeći način:

    a' = b
    b' = a % b

Obzirom da važi, na osnovu gornjeg tvrdjenja, da je:

    nzd(a', b') = nzd(b, a % b) = nzd(a, b)

a na osnovu induktivne hipoteze važi:

    nzd(m, n) = nzd(a, b)

važi i:

    nzd(a', b') = nzd(m, n)

što je i trebalo dokazati.

Da li se algoritam zaustavlja, to jest, da li će u nekom momentu za vrednost promenljive r važiti r ≤ 0?

Nakon svakog izvršenja bloka naredbi u okviru petlje promenljiva r ima strogo manju vrednost od prethodne, jer važi:

    r' = a % b
       = a % r < r

Dakle niz ostataka r je strogo opadajući niz nenegativnih celih brojeva, pa će nakon konačno mnogo koraka vrednost promenljive r postati 0.

Na osnovu svojstva invarijante, nakon poslednjeg izvršavanja naredbi iz tela petlje važiće: nzd(a, b) = nzd(m, n), a b = 0 te je nzd(a, b) = nzd(a, 0) = a, pa pošto algoritam vraća vrednost a to i jeste nzd zadatih brojeva.

Zadatak 2

Neka je P funkcija koja prirodni broj n preslikava u prirodni broj sa istim ciframa, ali u obrnutom poretku (npr: P(12345) = 54321). Konstruisati algoritam koji za ulaznu vrednost - prirodan broj n, izračunava vrednost P(n). Dokazati korektnost napisanog algoritma.

Rešenje:

    inverzija(n) {
        m = 0;
        k = n;
        i = 0;

        while (k > 0) {
            m = m * 10 + k % 10;
            k = k / 10;
            i++;
        }

        return m;
    }

Dokaz korektnosti ćemo izvesti za brojeve n koji se ne završavaju nulom.

Dokažimo primenom matematičke indukcije da je relacija

    n = k · 10ⁱ + P(m)

invarijanta petlje, tj. dokažimo da ova relacija važi pre ulaska u petlju i nakon svakog izvršenja bloka naredbi u okviru petlje. Takodje, dokažimo i da je tvrdjenje "i je broj cifara broja m" invarijanta petlje.

Baza: Za i = 0 (dakle pre prvog izvršavanja petlje) imamo:

    n = k · 10⁰ + P(m) = k + P(0) = n + 0

i broj m ima nula cifara (smatramo da broj 0 ima nula cifara) pa tvrdjenje važi.

Induktivni korak: Pretpostavimo da tvrdjenje važi za i (to jest da važi nakon i izvršavanja bloka naredbi u okviru petlje) i dokažimo da važi i za i + 1.

Dakle, na osnovu induktivne hipoteze važi: n = k · 10ⁱ + P(m)

Naredna vrednost promenljive k je k / 10, pa važi:

    k · 10ⁱ' + P(m') = (k / 10) · 10ⁱ⁺¹ + P(m · 10 + (k % 10))
                     = (k / 10) · 10ⁱ⁺¹ + P(m) + (k mod 10) · 10ⁱ
                     = ((k / 10) · 10 + (k % 10)) · 10ⁱ + P(m)
                     = k · 10ⁱ + P(m)
                     = n, na osnovu induktivne hipoteze

Pri prelasku na drugi red koristili smo induktivnu hipotezu da je i broj cifara broja m. Naravno, i ovo tvrdjenje treba dokazati za nove vrednosti m' i i'. Tvrdjenje važi, jer je i' = i + 1, m' = m · 10 + k % 10.

Dokažimo još i da se algoritam zaustavlja. Na početku je k > 0 prirodan broj i nakon svakog prolaska kroz petlju se smanjuje, tako da će u konačnom broju koraka dostići vrednost 0. Tada algoritam završava sa radom i za k = 0 imamo da je n = P(m), pa je P(n) = m (jer za svako x ∈ N važi: P(P(x)) = x), gde je P(n) funkcija koja prirodan broj n preslikava u prirodan broj sa istim ciframa, ali u obrnutom poretku).

Napomena: Ako bismo želeli da obuhvatimo i brojeve koji se završavaju jednom ili sa više nula, algoritam bi bio isti, ali bi dokaz morao da se izmeni. Umesto pomenute invarijante petlje, trebalo bi uzeti relaciju:

    n = k · 10ⁱ + P(m) · 10ʲ

gde je j broj nula kojima se završava broj n.

Zadatak 3

Konstruisati algoritam koji za dati dekadni broj odredjuje niz cifara koji odgovara njegovom oktalnom zapisu. Dokazati korektnost tog algoritma.

Rešenje:

Odgovarajući kod dat je pseudokodom (nalik na Pascal):

     oktcifre(n) {
         k = 0;
         nPom = n;

         while (nPom > 0) {
             b[k] = nPom % 8;
             k = k + 1;
             nPom = nPom / 8;
         }

         return b;
     }

Invarijanta petlje: Posmatrajmo broj nOkt čije su oktalne cifre dobijene nakon k prolazaka kroz while petlju. Tada je invarijanta petlje:

    n = nPom * 8ᵏ + nOkt

Pokažimo ovo indukcijom:

Baza: za k = 0, važi da nPom = n, nOkt = 0, te je ovo tvrdjenje tačno.

Induktivni korak: Neka je ovo tvrdjenje tačno za neko k i pokažimo da je tačno za k + 1.

U narednom prolasku kroz ciklus dobijaju se nove vrednosti nPom', nOkt' za koje važi:

    nPom' = nPom / 8
    nOkt' = (nPom % 8) * 8ᵏ + nOkt

Tada važi:

    nPom' ⋅ 8ᵏ⁺¹ + nOkt' = (nPom / 8) ⋅ 8ᵏ⁺¹ + (nPom % 8) ⋅ 8ᵏ + nOkt
                         = [(nPom / 8) * 8 + (nPom % 8)] * 8ᵏ + nOkt
                         = nPom * 8ᵏ + nOkt
                         = n, prema induktivnoj hipotezi.

Da li se algoritam zaustavlja? Tj. da li će u nekom momentu biti nPom ≤ 0? Niz vrednosti za nPom (kao celobrojni količnik pri deljenju) je monotono opadajući niz prirodnih brojeva, tako da će u nekom momentu postati nula.

Nakon poslednjeg prolaska kroz petlju biće nPom = 0, te dobijamo n = nOkt, pa je ispravnost algoritma dokazana.