Lyhyt MathCheck-ohje (uuteen välilehteen)
Ohjelmien saaminen toimimaan oikein on vaikeaa. Vuonna 1986 raportoidussa koetilanteessa vain 10 % ammattimaisista ohjelmoijista sai yksinkertaisen perusalgoritmin koodattua oikein, vaikka ylivuotoja ei katsottu virheiksi. Havainto on herättänyt paljon keskustelua ja jatkohavaintoja. Niihin tutustumisen voit halutessasi aloittaa tästä.
Siksi on kehitetty erityinen ajattelutapa, jolla ohjelmat saa toimimaan oikein. Tämä tehtävä on tarkoitettu ensimmäiseksi tutustumiseksi siihen.
Turvallinen asiointi verkkopankissa edellyttää tiedon salausta. Yksi laskutoimitus, jota nykyaikaisissa salausmenetelmissä tarvitaan, on an mod M, missä kaikki kolme lukua ovat isoja (esimerkiksi 300-numeroisia) ja mod tarkoittaa jakojäännöstä. Sen suorittaminen laskemalla n − 1 eli noin 10300 kertolaskua ja jakojäännöstä veisi aikaa melko monta maailmankaikkeuden ikää.
Yllä mainittua ajattelutapaa sovelletaan tässä tehtävässä algoritmiin, joka suorittaa laskun tarpeeksi nopeasti. Yksinkertaisuuden vuoksi jakojäännöksen laskeminen jätetään näyttämättä, mutta se on helppo lisätä algoritmin joka kierrokselle.
Sama algoritmi todistuksineen kuin tässä tehtävässä on käsitelty lyhyemmin Toronton yliopistossa ja virheen etsimistehtävän kautta Carnegie-Mellon yliopistossa.
Kerrataan aluksi pari asiaa.
Kun jaetaan kolme litraa eli 30 desilitraa limsaa tasan kahdeksalle ihmiselle, jokainen saa 3,75 desilitraa. Tässä käytettiin reaalilukujen jakolaskua. Kun jaetaan 30 ilmapalloa kahdeksalle ihmiselle niin tasan kuin mahdollista, niin jokainen saa kolme ja kuusi ilmapalloa jää yli. Nyt käytettiin kokonaislukujen jakolaskua. Jokaisen saama määrä on osamäärä ja ylijääneiden määrä on jakojäännös.
Monissa ohjelmointikielissä n / m tarkoittaa joko likimääräistä reaalilukujen jakolaskua tai kokonaislukujen osamäärää riippuen siitä, mitä tyyppiä n ja m ovat. Monissa ohjelmointikielissä jakojäännöstä merkitään n % m. (Varoitus: negatiivisilla kokonaisluvuilla nämä eivät välttämättä päde.) Tässä tehtävässä n / m tarkoittaa tarkkaa reaalilukujen jakolaskua. Merkitsemme kokonaislukujen osamäärää n div m ja jakojäännöstä n mod m.
Binääripotenssi näyttää tältä. Se on kopioitu oikealle alas, jotta se olisi käsillä myös kun alla oleva kopio on kadonnut ruudun yläreunan yläpuolelle.
1 x := 1
2 while n > 0 do
3 if n mod 2 = 1 then
4 n := n − 1
5 x := x · a
6 n := n div 2
7 a := a · a
Harmaalla kirjoitettua riviä 4 ei oikeasti tarvita, mutta sen lisääminen helpottaa algoritmista päättelemistä. Sen lisääminen ei muuta sitä arvoa, mikä rivillä 6 sijoitetaan n:ään, koska …rivin 3 ehdon vuoksi se suoritetaan vain kun n on pariton, ja silloin n div 2 = (n − 1) / 2 = (n − 1) div 2. (Miksi vihjeen yhtäsuuruudet pätevät? ensimmäinenn div 2 = (n − 1) / 2: tämän näimme edellä. toinen(n − 1) / 2 = (n − 1) div 2: jako menee tasan, joten / tuottaa saman tuloksen kuin div.) Mitään muutakaan vaikutusta sen lisäämisellä ei ole jatkoon, koska rivien 4 ja 6 välissä n:n arvoa ei käytetä mihinkään.
Ohjelmointitaidon osalta tässä tehtävässä riittää kyky tehdä päätelmiä yhden tai muutaman rivin vaikutuksesta, kuten tehtiin juuri äsken. Ei tarvitse tietää, miten binääripotenssi toimii kokonaisuutena. Saattaa olla jopa eduksi jos ei tiedä, koska se helpottaa ajattelun keskittämistä todistusmenetelmään ja kulloinkin todistettavaan pikkuasiaan, sen sijaan että vastauksia etsittäisiin binääripotenssin toimintaa koskevasta intuitiosta. Kuten alussa todettiin, intuitiomme ei ole luotettava.
Algoritmin tehtävänä on siis laskea AN, missä N on luonnollinen luku. Todistamme, että algoritmi laskee oikean lopputuloksen. Lopuksi selvitämme, suunnilleen kuinka nopeasti se toimii.
Käytämme silmukoiden todistamisessa hyvin yleistä päättelytapaa, jossa on viisi vaihetta:
Koska potenssilasku ei ole määritelty esimerkiksi silloin kun kantaluku on nolla ja eksponentti negatiivinen, meidän on pidettävä tarkkaan huolta, että väitteissämme eksponentit ovat aina ei-negatiivisia.
Vaiheen 3 hoitamiseksi oletamme, että invariantti ja silmukan ehto pätevät rivin 3 alussa, ja todistamme, että invariantti pätee rivin 7 lopussa. Tämän tehdäksemme alamme käydä silmukkaa läpi.
Vastatessasi edelliseen kohtaan huomasit ehkä, että tämän muodon voi päätellä suoraan, mutta voi olla vaikeaa miettiä pitääkö sijoituksen n := n − 1 vaikutus ottaa huomioon lisäämällä vai vähentämällä invariantissa n:ään ykkönen. Jos sijoituslauseen oikealla puolella on jotain monimutkaisempaa, vaikeus kasvaa. Siksi jätämme binääripotenssin hetkeksi, ja opettelemme kikan, jolla voidaan ratkaista seuraava ongelma:
Ohjelmassa on sijoituslause ja tunnetaan kaava, joka pätee juuri ennen sijoituslausetta. Johda mahdollisimman vahva kaava, joka pätee heti sijoituslauseen jälkeen.
Ennen sijoituslausetta voimassa oleva kaava kannattaa muuttaa muotoon, jossa sijoituslauseen oikea puoli esiintyy sellaisenaan. Tyypillisesti se esiintyy yhden kerran, mutta muutkin määrät ovat mahdollisia. Sijoituksen kohteena oleva muuttuja ei saa esiintyä muualla kuin näissä oikeissa puolissa. Sijoituslauseen jälkeinen tilanne saadaan korvaamalla ne muuttujalla, johon sijoitetaan.
Esimerkiksi sijoituslauseen n := 2n + 1 ja kaavan 4n = k tapauksessa se tarkoittaa, että ensin kaava muutetaan muotoon 2(2n + 1) − 2 = k. Tämä on loogisesti yhtäpitävä alkuperäisen kaavan kanssa, koska 2(2n + 1) − 2 = 4n. Sitten 2n + 1 korvataan n:llä, jolloin saadaan 2n − 2 = k. Tulokseksi saatiin, että jos ennen sijoitusta n := 2n + 1 päti 4n = k, niin sijoituksen jälkeen pätee 2n − 2 = k.
Seuraavaksi tarkastelemme tilannetta rivin 6 alussa. Vaikka rivin 4 mukana- tai poissaolo ei muuta algoritmin tulosta, alla oleviin väitteisiin se vaikuttaa. Oletamme, että rivi 4 on mukana. Näimme, että jos mentiin then-haaran kautta, niin invariantti oli välillä pois voimasta mutta astui uudelleen voimaan then-haaran lopussa. Jos then-haara ohitettiin, niin minkään muuttujan arvo ei muuttunut, joten invariantti pätee koska se päti rivin 3 alussa. Siis joka tapauksessa invariantti pätee rivin 6 alussa.
Olemme todistaneet, että jos silmukan vartaloon tullaan ja invariantti on voimassa sen alussa, niin se on voimassa myös silmukan vartalon lopussa. Siis vaihe 3 on valmis.
Silmukkaehtona on kuitenkin n > 0, joten algoritmi pysähtyy, koska …kun n > 0 pätee n div 2 ≤ n / 2 < n, joten n pienenee silmukan jokaisella kierroksella kunnes se on 0.
Koska kumpikin kahteen edelliseen laatikkoon kirjoittamistasi lausekkeista on yhtäsuuri lausekkeen xan kanssa, ne ovat yhtäsuuret myös keskenään, joten algoritmin tuottama vastaus on oikein. Vaihe 5 ja sitä myöten koko todistus on valmis.
Tämä algoritmi motivoitiin lupauksella nopeudesta, joten nyt on aika katsoa kuinka nopea se on. Algoritmin käyttämissä perusoperaatioissa ei ole mitään kertolaskua monimutkaisempaa. Kolmesataanumeroisten lukujen kertolasku ei ole yhtä pieni homma kuin kymmennumeroisten, joten tarkassa laskelmassa kiinnitettäisiin huomiota perusoperaatioiden hintaan. Nyt emme kuitenkaan ole niin tarkkoja, vaan katsomme ainoastaan silmukan kierrosten määrää.
Kolmesataanumeroisilla luvuilla tulee siis hiukan alle tuhat kierrosta. Tietokoneelle se on kohtuullinen työmäärä siitäkin huolimatta, että peruslaskutoimitukset tehdään 300-numeroisilla luvuilla.