Ohjelman oikeaksi todistaminen
Ohjelman oikeaksi todistaminen on ohjelmistotekniikassa tekniikka, jossa ohjelma todistetaan todeksi. Sen vastakohta ja huomattavasti yleisempi tapa on ohjelmantestaus. Tyypillisesti ja perinteisesti on katsottu, että ohjelman testaaminen verrattuna sen oikeaksi todistamiseen on kokonaisuutena edullisempaa. Ohjelman oikeaksi todistaminen on yleensä verrattaen iso tehtävä suhteessa itse ohjelman tekemiseen. Se voi olla jopa monin verroin suurempi, kun taas testaus voi minimissään olla olematon.
Todistamisen yleinen rakenne on yleensä seuraava.[1] Ohjelmalle laaditaan formaali määrittely. Alkuehtoon kuuluu ohjelman alkutila sekä syöttötiedot.[1] Loppuehto sisältää ohjelman lopputilan ja tulosteet.[1] Todistamisessa tulee osoittaa ohjelman toimivan siten, että alkuehdoista seuraa loppuehto kaikilla alkuehdoilla.[1]
Katso myös muokkaa
Lähteet muokkaa
- ↑ a b c d Ohjelmavirhe voi löytyä poikkeavalla tavalla Tivi. Viitattu 12.3.2016.
Aiheesta muualla muokkaa
- 8101160 OHJELMIEN TODISTAMINEN (Arkistoitu – Internet Archive)