Eukleideen algoritmin oikeellisuus

• Algoritmi ”pseudokoodina”:

  • Syöte: kokonaisluvut m0, n0 ³ 0.
  • Algoritmi:
    m ¬ m0 , n ¬ n0
    while n > 0 do
    
    r ¬ m mod n
    
    m ¬ n
    n ¬ r
    return m.

• Oikeellisuusväitteet:

  (i) Algoritmin suoritus päättyy kaikilla m0, n0 ³ 0.
  
  (ii) Algoritmin palauttama arvo on syt(m0, n0)

• Väite (i) voidaan todistaa tarkastamalla, että jos nɬ, niin silmukan suoritus pienentää n:n arvoa. (Koska 0 £ m mod n < n.)

• Väite (ii) seuraa soveltamalla seuraavaa silmukkainvarianttia: muuttujien m ja n arvot silmukan kunkin suorituskerran alussa toteuttavat ehdon:

  syt(m, n) = syt(m0, n0).
  
  [Invariantin säilymistodistus HT.]

Edellinen dia

Palaa ensimmäiseen diaan

Tarkastele graafista versiota