1  for i := 2 to n do
2      z := A[i]; j := i−1
3      while j > 0 && A[j] > z do
4          A[j+1] := A[j]
5          j := j−1
6      A[j+1] := z

Tehtävä:
Insertion sort

Lyhyt MathCheck-ohje (uuteen välilehteen)

Insertion sort on yksinkertainen algoritmi taulukon järjes­tämiseksi kasvavaan (tai vähenevään) suuruus­järjestykseen. Kuten kaikki muutkin yksin­kertaiset järjestämis­algoritmit, se on monilla syötteillä hidas (tarkemmin sanottuna neliöllinen). Muissa suhteissa se on hyvä, joten se on suositeltava valinta silloin, kun muut seikat ovat tärkeämpiä kuin nopeus.

”for i := 2 to n do 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 false, se palautetaan operaattorin tuloksena eikä oikeaa puolta lasketa lainkaan. Jos vasen puoli tuottaa true, lasketaan oikea puoli ja palautetaan sen tulos operaattorin tuloksena. Muiden algoritmissa käytettävien merkintöjen selitykset voit katsoa tehtävän Puolitus­haku alusta.

Insertion sort taulukolle A, jonka indeksit ovat 1, …, n, näyttää tältä:

1  for i := 2 to n do
2      z := A[i]; j := i−1
3      while j > 0 && A[j] > z do
4          A[j+1] := A[j]
5          j := j−1
6      A[j+1] := z

Se on kopioitu oikealle alas, jotta se olisi käsillä myös kun yllä oleva kopio on kadonnut ruudun yläreunan yläpuolelle.

Kirjoita predikaatti, joka kertoo, mitä i:n arvosta tiedetään, kun suoritus on rivin 2 alussa.
tai

Kirjoita predi­kaatti, joka sanoo, että taulukon alkuosa kohtaan i−1 asti on kasvavassa suuruus­järjestyksessä. Predikaatin täytyy sisältää myös edellä mainittu rajoite i:n arvolle. Jokin rajoite tarvitaan, koska väite ei ole mielekäs, jos esim. i = 0 tai i = n+2. Tässä tapauksessa on luontevinta valita edellä mainittu rajoite, koska se pätee ohjelmassa.

tai

Tämä predikaatti pätee aina kun suoritus on rivin 2 alussa.

Rivit 2, …, 6 siirtävät alkion A[i] oikealle paikalleen ja raivaavat sille tilaa siirtämällä yhden pykälän verran oikealle niitä alkioita, 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. Niin tekeminen tuottaa selkeämpiä virheilmoituksia. Siksi alla olevissa kohdissa älä käytä muuttujaa n äläkä lisää edellä mainittua rajoitetta muuttujalle i.

Rivin 3 alussa vallitsevaa tilannetta kannattaa ajatella seuraavasti:

  1. Kirjoita predikaattina, mitä tiedetään j:n arvosta. Ota pohdinnassasi huomioon, että kun rivin 3 alkuun tullaan viimeisen kerran, silmukan ehto j > 0 && A[j] > z ei toteudu.
    tai
  2. Alkion A[j+1] arvo on kopioitu joko z:aan tai A[j+2]:een, eikä sitä tulla enää lukemaan kohdasta j+1. Siksi kutsumme kohtaa j+1 ”vapaaksi”.
  3. Muuttujan z arvo kuuluu kohtaan, jonka paikka on j+1 tai vähemmän. Toisin sanoen, alkiot A[j+2], …, A[i] ovat suurempia kuin z. Kirjoita predikaatti, joka sanoo, että A[j+2], …, A[i] ovat suurempia kuin z ja lisäksi sanoo (a)-kohdan tiedon j:n arvosta.

    tai
  4. Kirjoita predikaattina, että muut paikoissa 1, …, i olevat alkiot kuin paikassa j+1 oleva ovat kasvavassa suuruus­järjestyksessä. Muista j:tä koskeva rajoite.

    tai

Rivin 5 alussa tilanne on hieman muuttunut äskeisestä:

  1. Kirjoita predikaattina, mitä tiedetään j:n arvosta.
    tai
  2. Vapaa paikka on . tai
  3. Kirjoita predikaatti, joka sanoo, että ne alkiot ovat suurempia kuin z jotka nyt tiedetään suuremmiksi kuin z, ja lisäksi sanoo (a)-kohdan tiedon j:n arvosta.

    tai
  4. Muunna myös rivin 3 alun predikaatti (d) rivin 5 alun tilanteen mukaiseksi.

    tai

Seuravaaksi tarvitsemme predikaatit ja vapaan paikan rivin 5 lopun tilanteen mukaisena. Jatkon kannalta on tärkeää, että sievennät (a)-kohdan muotoon, jossa vertailu­operaat­toreiden välissä esiintyy j yksinään (eikä esim. j−1).

  1. tai
  2. Vapaa paikka on . tai

  3. tai

  4. tai

Rivin 5 lopusta suoritus hyppää rivin 3 alkuun. Näin ollen voisi tuntua luontevalta, että rivin 5 lopussa pätevät samat predikaatit kuin rivin 3 alussa. Kuinka kävi?
(a) 5 loppu ⇐ 3 alku
(a) 5 loppu ⇔ 3 alku
(a) 5 loppu ⇒ 3 alku
(b) 5 loppu < 3 alku
(b) 5 loppu = 3 alku
(b) 5 loppu > 3 alku
(c) 5 loppu ⇐ 3 alku
(c) 5 loppu ⇔ 3 alku
(c) 5 loppu ⇒ 3 alku
(d) 5 loppu ⇐ 3 alku
(d) 5 loppu ⇔ 3 alku
(d) 5 loppu ⇒ 3 alku
tai

Ei siis saatu rivin 3 alun tilannetta kuvaavia predikaatteja (a), (c) ja (d) takaisin täysin samanlaisina rivin 5 lopussa. Sen sijaan saatiin tulokseksi, että jos ne ovat voimassa rivin 3 alussa, niin ne (ja jopa hieman vahvemmat predikaatit) ovat voimassa kun rivin 3 alkuun tullaan seuraavan kerran.

Seuraava tavoit­teemme on osoittaa, että ne ovat voimassa kun rivin 3 alkuun tullaan ensimmäisen kerran. Sitten kun sekin on osoitettu, tiedämme, että ne ovat voimassa aina kun ollaan rivin 3 alussa.

Kun rivin 3 alkuun tullaan ensimmäisen kerran, j = i−1 rivin 2 vuoksi.

  1. Sijoittamalla j:n paikalle i−1 rivin 3 alun (a)-predikaattiin saadaan . Sen toinen puoli on selvästi totta ja toinen seuraa aiemmin saadusta tiedosta 2 ≤ i ≤ n.
    tai
  2. 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.
  3. Alkioiksi, joiden kuuluu olla suurempia kuin z, tulee A[i−1+2], …, A[i] eli A[i+1], …, A[i]. Se on tyhjä luettelo alkioita, joten jokainen sen alkio todellakin on suurempi kuin z.
  4. (d)-kohdasta jää jäljelle vaatimus, että paikoissa 1, …, i−1 olevat alkiot ovat kasvavassa suuruus­järjestyksessä. Sen tarkastaminen edellyttää for-silmukan tutkimista. Palaamme siihen kohta. Sitä ennen meidän on tutkittava, mitä rivi 6 saa aikaan.

Riville 6 tullaan riviltä 3 ja vain siinä tapauksessa, että while-silmukan ehto ei toteutunut. Siksi rivin 6 alussa pätevät sekä rivin 3 alun väittämät (a), (b), (c) ja (d) että while-silmukan ehdon negaatio, jota merkitsemme (e). Minkä ansiosta seuraavat väittämät pätevät rivillä 6? Valitse kultakin riviltä enintään yksi ruutu.
(a)(b)(c)(d)(e)
z sijoitetaan paikkaan, jonka arvo on kopioitu muualle.
z:n sijoituspaikan oikealla puolella kohtaan i asti olevat alkiot ovat suurempia kuin z.
z:n sijoituspaikan vasemmalla puolella olevat alkiot ovat pienempiä kuin z.
Välittömästi z:n sijoituspaikan vasemmalla puolella joko ei ole alkiota tai siinä oleva alkio on korkeintaan yhtä suuri kuin z.
Kohdissa 1, …, i muualla kuin z:n sijoitus­paikassa sijait­sevat alkiot ovat kasvavassa suuruus­järjestyksessä.
tai

Jäljellä on enää for-silmukan todistaminen oikein toimivaksi. Totesimme aiemmin, että kun suoritus on rivin 2 alussa, taulukon alkuosa kohtaan i−1 asti on kasvavassa suuruus­järjestyksessä. Miksi tämä on voimassa for-silmukan ensimmäisellä kierroksella?
Se oletettiin algoritmin lähtötilanteesta.
Alkuosassa on silloin vain yksi alkio, joten se on automaattisesti kasvavassa suuruus­järjestyksessä.
Alkuosassa ei silloin ole yhtään alkiota, joten se on automaattisesti kasvavassa suuruus­järjestyksessä.
tai

Seuraava tehtävä on osoittaa, että jos taulukko oli järjestyksessä kohtaan i−1 asti for-silmukan kierroksen alkaessa, niin se on järjestyksessä kohtaan i asti for-silmukan kierroksen päättyessä. Tämän jos-osa lupaa sen asian, joka edellä jätettiin tutkittavaksi for-silmukan yhteydessä. Niin-osa saadaan suoraan riviä 6 koskevista johto­päätöksistämme. Näistä seuraa, että kun insertion sort lopettaa, taulukko on järjestyksessä kohtaan n saakka eli kokonaan.

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ä ilmaisu­tavasta, 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ä:

Täydellisessä todistuksessa osoitetaan myös, että silmukkaa ei voida jäädä kiertämään loputtomasti. Insertion sortin tapauksessa se on selvää, koska i kasvaa for-silmukan jokaisella kierroksella ja silmukka lopetetaan kun i > n, ja j pienenee while-silmukan jokaisella kierroksella ja silmukka lopetetaan kun j ≤ 0. Siksi siitä ei tehty kysymyksiä.

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 pikku­tarkkaa touhua, mutta välttämätöntä, jos haluamme saada aikaan luotettavia tehokkaita ohjelmia.