Puristukset

Tänään alkoi kolmannen syklin ykkösviikko, jota voi pitää ikäänkuin "juhlaviikkona" 5/3/1-ohjelmassa. Tämä viikko on ensimmäinen kun pääsen kilogrammamäärissä mitaten testaamaan uusia ennätyksiä.

Pystypunnerrus avasi pelin, ja tänään sain 2x59kg pystypunnerrettua. Ei siis mitään vauhtipunnerruksia tai pompautuksia; Vauhtipunnerruksella viitataan sellaiseen nostoon "suorille käsille", jossa tanko lähtee rinnalta ja jalat tekevät pompun muutta eivät liiku paikaltaan, esimerkiksi ei saksata. Pystypunnerrus on tyypillisesti noin 75% vauhtipunnerruksesta, eli vauhtipunnertamaan pitäisi pystyä noin 78 kiloa, joskin useimmat painonnostajat vauhtipunnertavat nykyisin enemmän kuin pystypunnertavat, koska pystypunnerrus tai "prässi" ei enää kuulu painonnostolajeihin.

Prässi on minulle ehdottomasti haastavin laji nelikosta. Siinä kehitys on hitainta koska siinä ketjun heikoin lenkki on kaikkein heikoin ja "kineettinen ketju" on kaikkein pisin: tanko pitää nostaa ylös ja tukipiste on maassa. Olympianostoissa on sama, mutta niissä tulos voi olla hieman korkeampi, koska niissä voi käyttää kropan vipuvarsia ja dynaamista voimantuotantoa.

Tänään jätettiin arvioitavaksi eräs paperi jossa olin kanssakirjoittajana. Se käsiteelee ns. puristusinvariantteja.

Lukijat voivat nyt vaihtaa kanavaa, jos eivät ole kiinnostuneita tietojenkäsittelystä ja logiikasta. Jos meillä on ohjelmakoodi S, niin ns. Hoaren kolmikko on {P} S {Q} joka ilmaisee seuraavaa: Jos väite P pätee ennen ohjelmakoodin suoritusta, niin väite Q pätee sen jälkeen. Hoaren kolmikkoja käytetään ilmaisemaan väittämiä tietokoneohjelmista; Hoaren kolmikko on siis väittämä joka joko pätee tai ei päde. P on tässä ns esiehto ja Q on jälkiehto.

Heikoin esiehto taas on ohjelmalle S ja jälkiehdolle Q heikoin sellainen väittämä P, että {P} S {Q} on voimassa. Heikoin tässä tarkoittaa sitä, että jos {R} S {Q} on myös voimassa, niin R:stä seuraa loogisesti P. Ohjelman toiminta voidaan logiikan mielessä tarkalleen määrittää määrittämällä jokaiselle ohjelman käskylle heikoin esiehto. heikointa esiehtoa merkitään wp(S,Q)

Vahvin jälkiehto on heikoimman esiehdon duaali. Vahvin jälkiehto ohjelmalle S ja esiehdolle P on sellainen väittämä Q, että jos {P} S {R} pätee, niin Q:sta seuraa loogisesti R. Ohjelman toiminta voidaan samaan tapaan määrittää tarkalleen etsimällä vahvin jälkiehto väittämälle P ja ohjelmalle S. vahvinta jälkiehtoa merkitään sp(P,S).  Pätee, että Q = sp(P,S) jos ja vain jos P = wp(S,Q).

Ohjelman semantiikka voidaan melkein kaikilta osin kiinnittää joko wp- tai sp- määritelmien avulla. Poikkeuksena ovat silmukat joille heikoimman esiehdon tai vahvimman jälkiehdon määritteleminen on ei-triviaali tehtävä. Itseasiassa, se on laskennallisesti ratkeamaton tehtävä yleisesti.

Voidaan kuitenkin joskus selvittää päteekö {P} X {Q} vaikka X:ssä olisi silmukka. Oletetaan nyt että ohjelma on muotoa "while R do S", eli silmukassa suoritetaan ohjelmanpätkää S niin kauan että R pysyy voimassa. Oletetaan että heikoin esiehto tai vahvin jälkiehto S:lle ja mielivaltaiselle väittämälle pystytään laskemaan.

Silmukalle voidaan etsiä invariantti I, jolla on seuraavat ominaisuudet: 1) {I} S {I} pätee,  2) P:stä seuraa I, ja 3) väittämästä I & !R seuraa Q. Kohta 1) sanoo että I on induktiivinen, so, jos se on kerran voimassa, niin jokainen silmukan kierros säilyttää sen voimassa. Kohta 2 sanoo että se pätee kun mennään silmukkaan ja kohta 3 takaa jälkiehdon toteutumisen.

Invariantin löytäminen ei yleisessä tapauksessa ole mahdollista. Logiikasta löytyy kuitenkin muutama työkalu jolla joskus invarintti saadaan napattua. On nimittäin pari juttua jotka huomataan: Jos kaksi kaavaa A ja B toteuttaa ensimmäisen ehdon, niin niiden konjuktio (A ja B) toteuttaa ensimmäisen kohdan myös, samoin kuin niiden disjunktio (A tai B). Lisäksi huomataan että jos ehto 2 pätee, niin kaavan heikentäminen (eli yleistäminen) ei riko kohtaa 2, ja jos ehto 3 pätee, niin kaavan vahvistaminen ei riko kohtaa 3.

Lisäksi meillä on ns Craigin interpolaatioteoreema: Jos kaavat A ja B ovat yhteensopimattomat, eli jos A & B on ristiriitainen, on olemassa ns. interpolaatiokaava C siten että A implikoi C:n (C on A:n aito yleistys), C:ssä esiintyy ainoastaan muuttujia jotka ovat yhteisiä A:lle ja B:lle, ja C & B on ristiriitainen.

Kehittämämme työkalu on ns. puristusinvarianttityökalu. Se toimii siten, että määritellään  A[0] = P, ja jokaisella i sovitaan että A[i] = sp(A[i-1] & R, S), eli A[i] tarkoittaa vahvinta väittämää joka pätee kun silmukkaa olisi ajettu i kertaa.  Samoin määritellään B[0] = !Q & !R ja B[i] = B[0] | wp(S,B[i-1]). Alussa näistä ei lasketa kuin yksi. B[i]:n tulkinta on että se on heikoin kaava joka päti viimeiset i kierrosta sitten siten, että silmukasta on tultu ulos ja Q ei ole ollut totta; eli että ohjelma on tehnyt "virheen".

Jos A[i] && B[i] *ei* ole ristiriitainen, vaan sille löytyy malli, niin ohjelma ei toteuta annettua Hoaren kolmikkoa; silmukkaa ajetaan i kierrosta, jonka aikana tapahtuu jotain mikä takaa että silmukasta tullaan ulos ja jälkiehto ei päde. Tämä voidaan tarkastaa kaavoista ns. SMT-ratkaisijalla; SMT-ratkaisijat ovat nykyisin varsin tehokkaita. Jos kaava ei ole ristiriitainen, SMT-ratkaisija palauttaa sellaiset muuttujien arvot joilla kaava pätee.

Jos se on ristiriitainen, niin  mitä tämä tarkoittaa? No, se tarkoittaa että mitä ikinä i:nnen kierroksen jälkeen pätee, niin *jos* silmukasta tullaan ulos, niin jälkiehdon on pakko päteä. Se ei takaa kuitenkaan että silmukasta tultaisiin ulos. Ainoastaan että jos tultiin, niin Q päti.

Se mitä tehdään, on joka kierroksella lasketaan interpolantti C väittämille A[i] ja B[i].  C on aito yleistys A[i]:sta, ja siinä esiintyy vain muuttujia jotka esiintyvät myös B[i]:ssä. Interpolantti takaa nyt ominaisuudet 1) ja 3), joten tarkistamme, onko se myös induktiivinen. Jos se on induktiivinen, niin olemme löytäneet invariantin joka todistaa ohjelman oikeaksi.

Jos taas kaava ei ole induktiivinen, niin jatketaan. Mutta nyt ei jatketa A[i]:sta, vaan otetaan C[i], eli interpolantti, ja lasketaan sille jälkiehtoja, C[i+1].

Nyt ongelmana on, että interpolantti C:stä lähtien voidaan päätyä tilanteeseen jossa C[j] && B[j] ei olekaan ristiriitainen. Jos näin käy, niin löydetty muuttujien arvoyhdistelmä voi olla tai olla olematta todistus sille, että ohjelma tekee virheen. Jos se on, niin hyvä, virhe voidaan raportoida. Jos se taas ei ole, niin joudutaan peruuttamaan takaisin A[i]:hin, ja laskemaan A[i+1], sensijaan että käytettäisiin interpolanttia. Tämä siksi, että on löydetty tilanne jossa meillä on abstrakti virhetilanne, joka ei todellisuudessa voikaan esiintyä. Tämä informaatio on hyödyllistä kyllä jossain mielessä, mutta se ei todista ohjelmaa vääräksi, joten ei voida lopettaa vielä.

Tässä kaikessa yksinkertaisuudessaan idea. Työkalumme päihittää useimmilla (ei kaikilla) benchmarkeilla ainakin BLAST:in, invGen:in, Interprocin ja HOLA:n, jotka nyt ovat viime vuosien työkaluista tutuimpia.

En voi ottaa tästä mitään kunniaa. Osallistuin tutkimukseen lähinnä esittämällä kysymyksiä ja ehdottamalla vaihtoehtoja eri tilanteisiin. Opin prosessissa kuitenkin aika paljon. Se oli mielenkiintoisinta.