Insertion sort on yksinkertainen algoritmi taulukon järjestämiseksi
suuruusjärjestykseen.
Kuten kaikki muutkin yksinkertaiset järjestämisalgoritmit, se on monilla
syötteillä hidas, tarkemmin sanottuna neliöllinen.
Muissa suhteissa se on hyvä, joten se on yleensä suositeltava valinta silloin,
kun neliöllinen suoritusaika riittää.
”fori := 2 tondo lauseita”
tarkoittaa, että lauseet suoritetaan ensin siten että i = 2,
seuraavaksi siten että i = 3 ja niin edelleen.
Viimeisellä kerralla i = n.
Operaattorin && vasen puoli lasketaan ensin.
Jos se tuottaa F, se palautetaan operaattorin tuloksena eikä oikeaa
puolta lasketa lainkaan.
Jos vasen puoli tuottaa T, lasketaan oikea puoli ja palautetaan sen
tulos operaattorin tuloksena.
Insertion sort taulukolle A, jonka indeksit ovat 1, …, n,
näyttää tältä:
Todistetaan, että silmukkainvariantti ja silmukan ehdon negaatio yhdessä
takaavat sen, minkä pitää päteä silmukan jälkeen.
while-silmukka
Tulemme for-silmukkaa todistaessamme osoittamaan, että tämä
predikaatti pätee aina kun suoritus on rivin 2 alussa.
Tässä alaluvussa tavoitteemme on osoittaa, että jos se pätee rivin 2
alussa, niin se pätee yhtä suuremmalle i rivin 6 lopussa.
Rivit 2, …, 6 siirtävät alkion A[i] alkuosaan
suuruusjärjestyksen mukaiselle paikalle ja raivaavat sille tilaa siirtämällä
yhden pykälän verran oikealle ne alkiot, jotka ovat jo järjestetyllä alueella
ja ovat arvoltaan suurempia kuin A[i].
Rivien 2, …, 6 toiminnan analysoimiseksi riittää tarkastella taulukon osaa
A[1…i] koko taulukon A[1…n] sijaan.
Teemme niin, koska niin on helpompaa.
Siksi alla olevissa kohdissa älä käytä muuttujaa n äläkä lisää edellä
mainittua rajoitetta muuttujalle i.
Ei siis saatu rivin 3 alun tilannetta kuvaavia predikaatteja (a), (c) ja
(d) takaisin täysin samanlaisina rivin 5 lopussa.
Sen sijaan saatiin hieman vahvemmat predikaatit, joissa j:n arvo on
rajattu hieman pienemmälle alueelle.
Koska vahvemmasta predikaatista seuraa heikompi predikaatti, saamme
tulokseksi, että rivin 3 alun tilannetta kuvaavat predikaatit (ja jopa hieman
vahvemmat predikaatit) ovat voimassa kun rivin 3 alkuun tullaan seuraavan
kerran.
Menetelmän vaihe 3 on valmis.
Seuraava tavoitteemme on osoittaa, että ne ovat voimassa kun rivin 3 alkuun
tullaan riviltä 2.
Sitten kun sekin on osoitettu, tiedämme, että ne ovat voimassa aina kun ollaan
rivin 3 alussa.
Sijoittamalla j:n paikalle i − 1 rivin 3 alun
tilanteeseen saadaan j + 1 = i − 1 + 1 = i siksi paikaksi,
jonka täytyy olla vapaa.
Ja sehän on vapaa, koska …A[i] kopioitiin z:aan rivillä 2.
Alkioiksi, joiden kuuluu olla suurempia kuin z, tulee
A[i − 1 + 2], …, A[i] eli A[i + 1], …,
A[i].
Jokainen sen alkio todellakin on suurempi kuin z, koska …se on tyhjä luettelo alkioita.
(d)-kohdasta jää jäljelle vaatimus, että …paikoissa 1, …, i − 1 olevat alkiot
ovat kasvavassa suuruusjärjestyksessä.
Invariantissa tämä vaadittiin muilta välin 1, …, i paikoilta kuin
j + 1.
Koska j = i − 1, paikka i jää pois
vaatimuksesta.
Tämä seuraa rivin 2 alun tilannetta koskevasta oletuksesta, jonka teimme
while-silmukan käsittelyn alussa lupauksella, että se tulee
todistetuksi for-silmukan käsittelyssä.
Nyt olemme rivin 3 alussa, mutta se ei haittaa, koska …väite puhuu vain muuttujien A ja i arvoista, ja
ne eivät muutu rivillä 2.
Menetelmän vaihe 2 on valmis.
Näistä seuraa, että paikoissa 1, …, i olevat alkiot ovat kasvavassa
suuruusjärjestyksessä rivin 6 lopussa.
Menetelmän vaihe 4 voidaan kuitata toteamuksella, että …j pienenee while-silmukan
jokaisella kierroksella ja silmukka lopetetaan kun j ≤ 0.
Olemme osoittaneet, että jos 2 ≤ i ≤ n ja paikoissa 1, …,
i − 1 olevat alkiot ovat kasvavassa suuruusjärjestyksessä rivin 2
alussa, niin paikoissa 1, …, i olevat alkiot ovat kasvavassa
suuruusjärjestyksessä rivin 6 lopussa.
for-silmukka
Jäljellä on enää for-silmukan todistaminen oikein toimivaksi.
Silmukka on yhtäpitävä seuraavan rakenteen kanssa:
0 i := 2
1 whilei ≤ ndo
…
7 i := i + 1
Todistamme sen osoittamalla, että seuraava on sen invariantti:
2 ≤ i ≤ n + 1 ja taulukon alkuosa kohtaan i − 1 asti on
kasvavassa suuruusjärjestyksessä.
Ensiksi hoidamme menetelmän vaiheen 2 eli ”kun silmukkaan
tullaan sen edeltä” -osan.
Tarvitseeko edes kysyä, miten osuus 2 ≤ i ≤ n + 1 todistetaan?
Tarvitsee!Se ei päde, jos n = 0.
Eikä silloin myöskään ”taulukon alkuosa kohtaan i − 1 asti” päde, vaan
on määrittelemätön.
Todistuksemme, jonka eteen olemme nähneet paljon vaivaa, ei siis päde, kun
n = 0.
Onneksi tapaus n = 0 voidaan todistaa helposti erikseen toteamalla,
että …silloin algoritmi ei tee
A:lle mitään ja se on oikein, koska silloin A on
tyhjä.
Kun n > 0, pätee 2 ≤ i ≤ n + 1 rivin 0 sijoituksen
i := 2 ansiosta.
Vaiheeksi 4 riittää huomautus, että i kasvaa for-silmukan
jokaisella kierroksella ja silmukka lopetetaan, kun i > n.
Kun insertion sort lopettaa, taulukko on järjestyksessä kohtaan i − 1
asti, missä i = n + 1.
Se on siis järjestyksessä kohtaan n saakka eli kokonaan.
Se oli vaihe 5.
Algoritmien todistamisessa ei läheskään aina kirjoiteta sellaisia
formaaleja predikaatteja kuin edellä, mutta niiden ilmaisema asia kylläkin
ilmaistaan jollain tavalla.
Riippumatta käytetystä ilmaisutavasta, asioiden ilmaiseminen riittävän
täsmällisesti on aluksi vaikeaa ja edellyttää harjoittelua, joka voi olla
tylsää.
Todistuksen rakenne on usein juuri sellainen kuin edellä.
Usein todistuksissa tarvitaan apuväittämiä varmistamaan, että
predikaateissa esiintyvät muuttujat ovat laillisella alueella ja predikaatit
siten ovat hyvin määriteltyjä.
(a)-kohtien predikaatit olivat tällaisia.
Niille ei löytynyt tehtävää kun kysyttiin, mihin kohtia (a), (b), (c), (d) ja
(e) tarvittiin, mutta ne olivat tarpeen muitten kohtien predikaattien osana.
Algoritmien todistaminen on pikkutarkkaa touhua, mutta välttämätöntä, jos
haluamme saada aikaan luotettavia tehokkaita ohjelmia.