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

Teh­tä­vä:
Insertion sort

Ly­hyt Math­Check-oh­je (uu­teen vä­li­leh­teen)

Insertion sort on yk­sin­ker­tai­nen al­go­rit­mi tau­lu­kon jär­jes­tä­mi­sek­si suu­ruus­jär­jes­tyk­seen. Ku­ten kaik­ki muut­kin yk­sin­ker­tai­set jär­jes­tä­mis­al­go­rit­mit, se on mo­nil­la syöt­teil­lä hi­das, tar­kem­min sa­not­tu­na ne­liöl­li­nen. Muis­sa suh­teis­sa se on hy­vä, jo­ten se on yleen­sä suo­si­tel­ta­va va­lin­ta sil­loin, kun ne­liöl­li­nen suo­ri­tus­ai­ka riit­tää.

for i := 2 to n do lau­sei­ta” tar­koit­taa, et­tä lau­seet suo­ri­te­taan en­sin si­ten et­tä i = 2, seu­raa­vak­si si­ten et­tä i = 3 ja niin edel­leen. Vii­mei­sel­lä ker­ral­la i = n. Ope­raat­to­rin && va­sen puo­li las­ke­taan en­sin. Jos se tuot­taa F, se pa­lau­te­taan ope­raat­to­rin tu­lok­se­na ei­kä oi­keaa puol­ta las­ke­ta lain­kaan. Jos va­sen puo­li tuot­taa T, las­ke­taan oi­kea puo­li ja pa­lau­te­taan sen tu­los ope­raat­to­rin tu­lok­se­na.

Insertion sort tau­lu­kol­le A, jon­ka in­dek­sit ovat 1, …, n, näyt­tää täl­tä:

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 ko­pioi­tu oi­keal­le alas, jot­ta se oli­si kä­sil­lä myös kun yl­lä ole­va ko­pio on ka­don­nut ruu­dun ylä­reu­nan ylä­puo­lel­le.

Al­go­rit­mis­sa on kak­si si­säk­käis­tä sil­muk­kaa. Sil­mu­koi­den oi­keak­si osoit­ta­mis­ta var­ten on vii­si­koh­tai­nen me­ne­tel­mä:

  1. Kek­si­tään kul­le­kin sil­mu­kal­le väit­tä­mä, jol­la päät­te­ly saa­daan on­nis­tu­maan. Si­tä kut­su­taan sil­muk­ka­in­va­rian­tik­si.
  2. To­dis­te­taan, et­tä sil­muk­ka­in­va­riant­ti pä­tee, kun sil­muk­kaan tul­laan sil­mu­kan edel­tä.
  3. To­dis­te­taan, et­tä jos sil­muk­ka­in­va­riant­ti pä­ti sil­mu­kan kier­rok­sen alus­sa, se pä­tee myös kun sil­mu­kan al­kuun tul­laan seu­raa­van ker­ran. Täs­sä to­dis­tuk­ses­sa voi­daan hyö­dyn­tää si­tä, et­tä sil­mu­kan eh­to pä­tee (muu­toin­han ei ol­tai­si teh­ty kier­ros­ta sil­mu­kas­sa vaan ol­tai­siin tul­tu ulos sil­mu­kas­ta).
  4. To­dis­te­taan, et­tä sil­mu­kan suo­ri­tus lop­puu jos­kus.
  5. To­dis­te­taan, et­tä sil­muk­ka­in­va­riant­ti ja sil­mu­kan eh­don ne­gaa­tio yh­des­sä ta­kaa­vat sen, min­kä pi­tää pä­teä sil­mu­kan jäl­keen.

while-sil­muk­ka

Kä­sit­te­lem­me while-sil­mu­kan en­sin. Al­ku­val­mis­te­lu­na sil­le, kir­joi­ta pre­di­kaat­ti, jo­ka ker­too, mi­tä i:n ar­vos­ta tie­de­tään, kun suo­ri­tus on ri­vin 2 alus­sa.
tai

Kir­joi­ta pre­di­kaat­ti, jo­ka sa­noo, et­tä tau­lu­kon al­ku­osa koh­taan i − 1 as­ti on kas­va­vas­sa suu­ruus­jär­jes­tyk­ses­sä. Pre­di­kaa­tin täy­tyy si­säl­tää myös edel­lä mai­nit­tu ra­joi­te i:n ar­vol­le. Jo­kin ra­joi­te tar­vi­taan, kos­ka väi­te ei ole mie­le­käs, jos esim. i = 0 tai i = n + 2. Täs­sä ta­pauk­ses­sa on luon­te­vin­ta va­li­ta edel­lä mai­nit­tu ra­joi­te, kos­ka se pä­tee oh­jel­mas­sa.

tai

Tu­lem­me for-sil­muk­kaa to­dis­taes­sam­me osoit­ta­maan, et­tä tä­mä pre­di­kaat­ti pä­tee ai­na kun suo­ri­tus on ri­vin 2 alus­sa. Täs­sä ala­lu­vus­sa ta­voit­teem­me on osoit­taa, et­tä jos se pä­tee ri­vin 2 alus­sa, niin se pä­tee yh­tä suu­rem­mal­le i ri­vin 6 lo­pus­sa.

Ri­vit 2, …, 6 siir­tä­vät al­kion A[i] al­ku­osaan suu­ruus­jär­jes­tyk­sen mu­kai­sel­le pai­kal­le ja rai­vaa­vat sil­le ti­laa siir­tä­mäl­lä yh­den py­kä­län ver­ran oi­keal­le ne al­kiot, jot­ka ovat jo jär­jes­te­tyl­lä alueel­la ja ovat ar­vol­taan suu­rem­pia kuin A[i]. Ri­vien 2, …, 6 toi­min­nan ana­ly­soi­mi­sek­si riit­tää tar­kas­tel­la tau­lu­kon osaa A[1…i] ko­ko tau­lu­kon A[1…n] si­jaan. Teem­me niin, kos­ka niin on hel­pom­paa. Sik­si al­la ole­vis­sa koh­dis­sa älä käy­tä muut­tu­jaa n älä­kä li­sää edel­lä mai­nit­tua ra­joi­tet­ta muut­tu­jal­le i.

Ri­vin 3 while-sil­mu­kan to­dis­ta­mi­sek­si oi­keak­si käy­täm­me in­va­riant­tia, jo­ka koos­tuu nel­jäs­tä osas­ta:

  1. Kir­joi­ta pre­di­kaat­ti­na, mi­tä ri­vin 3 alus­sa tie­de­tään j:n ar­vos­ta.
    tai
  2. Al­kion A[ j + 1] ar­vo on ko­pioi­tu jo­ko z:aan tai A[ j + 2]:een, ei­kä si­tä tul­la enää lu­ke­maan koh­das­ta j + 1. Sik­si kut­sum­me koh­taa j + 1 ”va­paak­si”.
  3. Muut­tu­jan z ar­vo kuu­luu koh­taan, jon­ka paik­ka on j + 1 tai vä­hem­män. Toi­sin sa­noen, al­kiot A[ j + 2], …, A[i] ovat suu­rem­pia kuin z. Kir­joi­ta pre­di­kaat­ti, jo­ka sa­noo, et­tä A[ j + 2], …, A[i] ovat suu­rem­pia kuin z ja li­säk­si sa­noo (a)-koh­dan tie­don j:n ar­vos­ta.

    tai
  4. Kir­joi­ta pre­di­kaat­ti­na, et­tä muut pai­kois­sa 1, …, i ole­vat al­kiot kuin pai­kas­sa j + 1 ole­va ovat kas­va­vas­sa suu­ruus­jär­jes­tyk­ses­sä. Muis­ta j:tä kos­ke­va ra­joi­te (a)-koh­das­ta.

    tai

To­dis­tam­me nyt, et­tä tä­mä in­va­riant­ti säi­lyy voi­mas­sa while-sil­mu­kan kier­rok­sen ai­ka­na, ja sen jäl­keen to­dis­tam­me, et­tä se on voi­mas­sa, kun ri­vil­le 3 tul­laan ri­vil­tä 2. Ri­vin 5 alus­sa ti­lan­ne on hie­man muut­tu­nut äs­kei­ses­tä:

  1. Kir­joi­ta pre­di­kaat­ti­na, mi­tä tie­de­tään j:n ar­vos­ta.
    tai
  2. Va­paa paik­ka on . tai
  3. Kir­joi­ta pre­di­kaat­ti, jo­ka sa­noo, et­tä ne al­kiot ovat suu­rem­pia kuin z jot­ka nyt tie­de­tään suu­rem­mik­si kuin z, ja li­säk­si sa­noo (a)-koh­dan tie­don j:n ar­vos­ta.

    tai
  4. Muun­na myös ri­vin 3 alun pre­di­kaat­ti (d) ri­vin 5 alun ti­lan­teen mu­kai­sek­si.

    tai

Seu­raa­vak­si tar­vit­sem­me pre­di­kaa­tit ja va­paan pai­kan ri­vin 5 lo­pun ti­lan­teen mu­kai­se­na. Jat­kon kan­nal­ta on tär­keää, et­tä sie­ven­nät (a)-koh­dan muo­toon, jos­sa ver­tai­lu­ope­raat­to­rei­den vä­lis­sä esiin­tyy j yk­si­nään (ei­kä esi­mer­kik­si j − 1).

  1. tai
  2. Va­paa paik­ka on . tai

  3. tai

  4. tai

Ri­vin 5 lo­pus­ta suo­ri­tus hyp­pää ri­vin 3 al­kuun. Näin ol­len voi­si tun­tua luon­te­val­ta, et­tä ri­vin 5 lo­pus­sa pä­te­vät sa­mat pre­di­kaa­tit kuin ri­vin 3 alus­sa. Kuin­ka kä­vi?
(a) 5 lop­pu ⇐ 3 al­ku
(a) 5 lop­pu ⇔ 3 al­ku
(a) 5 lop­pu ⇒ 3 al­ku
(b) 5 lop­pu < 3 al­ku
(b) 5 lop­pu = 3 al­ku
(b) 5 lop­pu > 3 al­ku
(c) 5 lop­pu ⇐ 3 al­ku
(c) 5 lop­pu ⇔ 3 al­ku
(c) 5 lop­pu ⇒ 3 al­ku
(d) 5 lop­pu ⇐ 3 al­ku
(d) 5 lop­pu ⇔ 3 al­ku
(d) 5 lop­pu ⇒ 3 al­ku
tai

Ei siis saa­tu ri­vin 3 alun ti­lan­net­ta ku­vaa­via pre­di­kaat­te­ja (a), (c) ja (d) ta­kai­sin täy­sin sa­man­lai­si­na ri­vin 5 lo­pus­sa. Sen si­jaan saa­tiin hie­man vah­vem­mat pre­di­kaa­tit, jois­sa j:n ar­vo on ra­jat­tu hie­man pie­nem­mäl­le alueel­le. Kos­ka vah­vem­mas­ta pre­di­kaa­tis­ta seu­raa hei­kom­pi pre­di­kaat­ti, saam­me tu­lok­sek­si, et­tä ri­vin 3 alun ti­lan­net­ta ku­vaa­vat pre­di­kaa­tit (ja jo­pa hie­man vah­vem­mat pre­di­kaa­tit) ovat voi­mas­sa kun ri­vin 3 al­kuun tul­laan seu­raa­van ker­ran. Me­ne­tel­män vai­he 3 on val­mis.

Seu­raa­va ta­voit­teem­me on osoit­taa, et­tä ne ovat voi­mas­sa kun ri­vin 3 al­kuun tul­laan ri­vil­tä 2. Sit­ten kun se­kin on osoi­tet­tu, tie­däm­me, et­tä ne ovat voi­mas­sa ai­na kun ol­laan ri­vin 3 alus­sa.

Kun ri­vin 3 al­kuun tul­laan ri­vil­tä 2,
j = tai
  1. Si­joit­ta­mal­la j:n pai­kal­le i − 1 ri­vin 3 alun (a)-pre­di­kaat­tiin saa­daan . Sen toi­nen puo­li on sel­väs­ti tot­ta ja toi­nen seu­raa aiem­min saa­dus­ta tie­dos­ta 2 ≤ in.
    tai
  2. Si­joit­ta­mal­la j:n pai­kal­le i − 1 ri­vin 3 alun ti­lan­tee­seen saa­daan j + 1 = i − 1 + 1 = i sik­si pai­kak­si, jon­ka täy­tyy ol­la va­paa. Ja se­hän on va­paa, kos­ka A[i] ko­pioi­tiin z:aan ri­vil­lä 2.
  3. Al­kioik­si, joi­den kuu­luu ol­la suu­rem­pia kuin z, tu­lee A[i − 1 + 2], …, A[i] eli A[i + 1], …, A[i]. Jo­kai­nen sen al­kio to­del­la­kin on suu­rem­pi kuin z, kos­ka se on tyh­jä luet­te­lo al­kioi­ta.
  4. (d)-koh­das­ta jää jäl­jel­le vaa­ti­mus, et­tä pai­kois­sa 1, …, i − 1 ole­vat al­kiot ovat kas­va­vas­sa suu­ruus­jär­jes­tyk­ses­sä. In­va­rian­tis­sa tä­mä vaa­dit­tiin muil­ta vä­lin 1, …, i pai­koil­ta kuin j + 1. Kos­ka j = i − 1, paik­ka i jää pois vaa­ti­muk­ses­ta. Tä­mä seu­raa ri­vin 2 alun ti­lan­net­ta kos­ke­vas­ta ole­tuk­ses­ta, jon­ka teim­me while-sil­mu­kan kä­sit­te­lyn alus­sa lu­pauk­sel­la, et­tä se tu­lee to­dis­te­tuk­si for-sil­mu­kan kä­sit­te­lys­sä. Nyt olem­me ri­vin 3 alus­sa, mut­ta se ei hait­taa, kos­ka väi­te pu­huu vain muut­tu­jien A ja i ar­vois­ta, ja ne ei­vät muu­tu ri­vil­lä 2.

Me­ne­tel­män vai­he 2 on val­mis.

Vai­heen 5 hoi­ta­mi­sek­si mei­dän on tut­kit­ta­va, mi­tä ri­vi 6 saa ai­kaan. Ri­vil­le 6 tul­laan ri­vil­tä 3 ja vain sii­nä ta­pauk­ses­sa, et­tä while-sil­mu­kan eh­to ei to­teu­tu­nut. Sik­si ri­vin 6 alus­sa pä­te­vät se­kä ri­vin 3 alun väit­tä­mät (a), (b), (c) ja (d) et­tä while-sil­mu­kan eh­don ne­gaa­tio, jo­ta mer­kit­sem­me (e). Min­kä an­sios­ta seu­raa­vat väit­tä­mät pä­te­vät ri­vil­lä 6? Va­lit­se kul­ta­kin ri­vil­tä enin­tään yk­si ruu­tu.
(a)(b)(c)(d)(e)
z si­joi­te­taan paik­kaan, jon­ka ar­vo on ko­pioi­tu muual­le.
z:n si­joi­tus­pai­kan oi­keal­la puo­lel­la koh­taan i as­ti ole­vat al­kiot ovat suu­rem­pia kuin z.
z:n si­joi­tus­pai­kan va­sem­mal­la puo­lel­la ole­vat al­kiot ovat pie­nem­piä kuin z.
Vä­lit­tö­mäs­ti z:n si­joi­tus­pai­kan va­sem­mal­la puo­lel­la jo­ko ei ole al­kio­ta tai sii­nä ole­va al­kio on kor­kein­taan yh­tä suu­ri kuin z.
Koh­dis­sa 1, …, i muual­la kuin z:n si­joi­tus­pai­kas­sa si­jait­se­vat al­kiot ovat kas­va­vas­sa suu­ruus­jär­jes­tyk­ses­sä.
tai

Näis­tä seu­raa, et­tä pai­kois­sa 1, …, i ole­vat al­kiot ovat kas­va­vas­sa suu­ruus­jär­jes­tyk­ses­sä ri­vin 6 lo­pus­sa.

Me­ne­tel­män vai­he 4 voi­daan kui­ta­ta to­tea­muk­sel­la, et­tä j pie­ne­nee while-sil­mu­kan jo­kai­sel­la kier­rok­sel­la ja sil­muk­ka lo­pe­te­taan kun j ≤ 0.

Olem­me osoit­ta­neet, et­tä jos 2 ≤ in ja pai­kois­sa 1, …, i − 1 ole­vat al­kiot ovat kas­va­vas­sa suu­ruus­jär­jes­tyk­ses­sä ri­vin 2 alus­sa, niin pai­kois­sa 1, …, i ole­vat al­kiot ovat kas­va­vas­sa suu­ruus­jär­jes­tyk­ses­sä ri­vin 6 lo­pus­sa.

for-sil­muk­ka

Jäl­jel­lä on enää for-sil­mu­kan to­dis­ta­mi­nen oi­kein toi­mi­vak­si. Sil­muk­ka on yh­tä­pi­tä­vä seu­raa­van ra­ken­teen kans­sa:

0  i := 2
1  while in do
       …
7      i := i + 1

To­dis­tam­me sen osoit­ta­mal­la, et­tä seu­raa­va on sen in­va­riant­ti:

2 ≤ in + 1 ja tau­lu­kon al­ku­osa koh­taan i − 1 as­ti on kas­va­vas­sa suu­ruus­jär­jes­tyk­ses­sä.

En­sik­si hoi­dam­me me­ne­tel­män vai­heen 2 eli ”kun sil­muk­kaan tul­laan sen edel­tä” -osan. Tar­vit­see­ko edes ky­syä, mi­ten osuus 2 ≤ in + 1 to­dis­te­taan? Tar­vit­see!Se ei pä­de, jos n = 0. Ei­kä sil­loin myös­kään ”tau­lu­kon al­ku­osa koh­taan i − 1 as­ti” pä­de, vaan on mää­rit­te­le­mä­tön. To­dis­tuk­sem­me, jon­ka eteen olem­me näh­neet pal­jon vai­vaa, ei siis pä­de, kun n = 0. On­nek­si ta­paus n = 0 voi­daan to­dis­taa hel­pos­ti erik­seen to­tea­mal­la, et­tä sil­loin al­go­rit­mi ei tee A:lle mi­tään ja se on oi­kein, kos­ka sil­loin A on tyh­jä. Kun n > 0, pä­tee 2 ≤ in + 1 ri­vin 0 si­joi­tuk­sen i := 2 an­sios­ta.

Väi­tim­me aiem­min, et­tä kun suo­ri­tus on ri­vin 2 alus­sa, tau­lu­kon al­ku­osa koh­taan i − 1 as­ti on kas­va­vas­sa suu­ruus­jär­jes­tyk­ses­sä. Mik­si tä­mä on voi­mas­sa for-sil­mu­kan en­sim­mäi­sel­lä kier­rok­sel­la?
Se ole­tet­tiin al­go­rit­min läh­tö­ti­lan­tees­ta.
Al­ku­osas­sa on sil­loin vain yk­si al­kio, jo­ten se on au­to­maat­ti­ses­ti kas­va­vas­sa suu­ruus­jär­jes­tyk­ses­sä.
Al­ku­osas­sa ei sil­loin ole yh­tään al­kio­ta, jo­ten se on au­to­maat­ti­ses­ti kas­va­vas­sa suu­ruus­jär­jes­tyk­ses­sä.
tai

In­va­riant­ti­to­dis­tuk­sen vai­he 3 eli ”säi­lyy voi­mas­sa” -osa hoi­det­tiin ala­lu­vus­sa while-sil­muk­ka mel­kein val­miik­si. Siel­lä to­dis­tet­tiin, et­tä jos tau­luk­ko oli jär­jes­tyk­ses­sä koh­taan i − 1 as­ti for-sil­mu­kan kier­rok­sen al­kaes­sa, niin se on jär­jes­tyk­ses­sä koh­taan i as­ti for-sil­mu­kan kier­rok­sen päät­tyes­sä. Jäl­kim­mäi­nen väi­te pa­laa ri­vil­lä 7 väit­teek­si muo­toa ”koh­taan i − 1 as­ti”. Väi­te 2 ≤ in + 1 muut­tuu ri­vil­le 2 tul­taes­sa muo­toon i ja ri­vil­lä 7 muo­toon i , jo­sta 2 ≤ in + 1 seu­raa.
tai

Vai­heek­si 4 riit­tää huo­mau­tus, et­tä i kas­vaa for-sil­mu­kan jo­kai­sel­la kier­rok­sel­la ja sil­muk­ka lo­pe­te­taan, kun i > n.

Kun insertion sort lo­pet­taa, tau­luk­ko on jär­jes­tyk­ses­sä koh­taan i − 1 as­ti, mis­sä i = n + 1. Se on siis jär­jes­tyk­ses­sä koh­taan n saak­ka eli ko­ko­naan. Se oli vai­he 5.

Al­go­rit­mien to­dis­ta­mi­ses­sa ei lä­hes­kään ai­na kir­joi­te­ta sel­lai­sia for­maa­le­ja pre­di­kaat­te­ja kuin edel­lä, mut­ta nii­den il­mai­se­ma asia kyl­lä­kin il­mais­taan jol­lain ta­val­la. Riip­pu­mat­ta käy­te­tys­tä il­mai­su­ta­vas­ta, asioi­den il­mai­se­mi­nen riit­tä­vän täs­mäl­li­ses­ti on aluk­si vai­keaa ja edel­lyt­tää har­joit­te­lua, jo­ka voi ol­la tyl­sää. To­dis­tuk­sen ra­ken­ne on usein juu­ri sel­lai­nen kuin edel­lä.

Usein to­dis­tuk­sis­sa tar­vi­taan apu­väit­tä­miä var­mis­ta­maan, et­tä pre­di­kaa­teis­sa esiin­ty­vät muut­tu­jat ovat lail­li­sel­la alueel­la ja pre­di­kaa­tit si­ten ovat hy­vin mää­ri­tel­ty­jä. (a)-koh­tien pre­di­kaa­tit oli­vat täl­lai­sia. Niil­le ei löy­ty­nyt teh­tä­vää kun ky­syt­tiin, mi­hin koh­tia (a), (b), (c), (d) ja (e) tar­vit­tiin, mut­ta ne oli­vat tar­peen muit­ten koh­tien pre­di­kaat­tien osa­na.

Al­go­rit­mien to­dis­ta­mi­nen on pik­ku­tark­kaa tou­hua, mut­ta vält­tä­mä­tön­tä, jos ha­luam­me saa­da ai­kaan luo­tet­ta­via te­hok­kai­ta oh­jel­mia.