Potenssiinkorotusalgoritmin oikeellisuus

• Algoritmi ”pseudokoodina”:

  • Syöte: kokonaisluku n ³ 0.
  • Algoritmi:
    m ¬ 1, i ¬ n
    
    while i > 0 do
    m ¬ 2*m
    i ¬ i-1
    output m.

• Oikeellisuusväitteet:

  (i) Algoritmin suoritus päättyy kaikilla n ³ 0.
  
  (ii) Algoritmin palauttama arvo on m = 2n.

• Väite (i) on voimassa, koska silmukkamuuttujan i arvo on ei-negatiivinen kokonaisluku, jota pienennetään jokaisella silmukan suorituskerralla. Tämä on mahdollista vain äärellisen monta kertaa.

• Väitteen (ii) todistus perustuu siihen, että while-silmukan suorittaminen säilyttää seuraavan silmukkainvariantin: muuttujien m ja i arvot silmukan kunkin suorituskerran alussa toteuttavat ehdon:

  I = {m*2i = 2n}.
  

Edellinen dia

Seuraava dia

Palaa ensimmäiseen diaan

Tarkastele graafista versiota