Ohjelmien ekvivalenttiuden selvittäminen

Abstract

Ohjelmien ekvivalenttiuden selvittäminen on paljon tutkittu aihe sen monista sovellusalueista johtuen. Sitä voidaan hyödyntää ohjelmien testaamisessa, refaktoroinnissa, verifioinnissa ja kääntäjien tekemien optimointien tarkastamisessa. Ongelma on todistettavasti ratkeamaton, eli yleispätevää ohjelmien ekvivalenttiuden selvittävää algoritmia ei voi olla. Tästä huolimatta monet tutkimusyhteisöt ovat esittäneet tutkimaansa rajalliseen sovellusalueeseen tarkoitettuja menetelmiä ohjelmien ekvivalenttiuden selvittämiseen, ja kehittäneet niihin perustuvia automaattisia työkaluja. Tämä tutkielma on kirjallisuuskatsaus, jossa tarkastellaan näitä menetelmiä. Kaikkia mahdollisia ohjelmien ekvivalenttiuden selvittämisen menetelmiä ei tässä työssä voida esittää. Katsaus on rajattu siten, että tarkasteltavaksi valittiin vain sellaisia menetelmiä, joista on useampia julkaisuja eri tutkijaryhmiltä. Valitut menetelmät ovat bisimilaarisuus, tulo-ohjelmat ja mallintarkastus. Menetelmistä esitetään niiden teoria, toteutus algoritmisesti sekä niiden vahvuudet ja heikkoudet.

Ohjelmien ekvivalenttiuden selvittämisen ongelmasta, sen sovellusalueista ja ekvivalenttiuden selvittämisen menetelmien arvioinnista puhutaan johdantoluvussa. Valittujen menetelmien käsittelyä ennen työssä esitellään ensin vaaditut pohjatiedot ohjelmien ekvivalenttiuden tarkastelemiseen. Ensin kerrotaan, miten ohjelmien toimintaa voidaan kuvata formaalisti, minkä jälkeen määritellään, mitä ohjelmien ekvivalenttiudella tarkoitetaan. Tämän jälkeen esitellään valitut ekvivalenttiuden selvittämisen menetelmät. Yksittäisiä menetelmiä käsittelevissä luvuissa esitellään ensin teoria niiden toiminnalle, minkä jälkeen esitetään algoritminen toteutus ohjelmien ekvivalenttiuden selvittämiseen kyseisellä menetelmällä. Lopuksi kerrotaan menetelmän heikkouksista ja menetelmään liittyvästä julkaistusta kirjallisuudesta.

Työssä nähdään, miten nykyiset menetelmät eroavat toiminnaltaan, ja miten ne soveltuvat eri käyttötarkoituksiin. Menetelmistä selviää, mitä ongelmia niissä on vielä ratkottavana, ja millaista uutta tutkimusta niistä mahdollisesti julkaistaan.