Naredna: FaktorijelGore: Uvod Prethodna: Algoritmi, pseudokod i dijagrami toka  Sadržaj

Formalno ispitivanje ispravnosti programa
- Metoda induktivne invarijante -

Formalna verifikacija se ne zasniva na testiranju i eksperimentima, već na matematičkim dokazima. Korektnost programa je dokaziva ako se u okviru nekog formalnog deduktivnog sistema može izvesti matematički dokaz da program zadovoljava zadatu specifikaciju.

Postoje tri dominantna pristupa formalnoj verifikaciji programa:

  1. metoda induktivne invarijante
  2. metoda funkcionalne semantike
  3. metoda eksplicitne semantike
Prva metoda je daleko najzastupljenija i do sada je dala najbolje rezultate, pa ćemo se u nastavku baviti samo njom. Ova metoda verifikacije programa se često nazova Flojd-Horov (Floyd-Hoare) metoda induktivnih tvrđenja i ima svoje korene u klasičnim radovima Goldstajna (Goldstine) i Fon Nojmana (von Neumann).

Za ispitivanje ispravnosti programa posebnu pažnju potrebno je posvetiti petljama jer se kroz njih može proći različit broj puta u različitim izvršavanjima programa.

Definicija 1. Svojstvo koje važi svaki put kada se ispituje da li je zadovoljen uslov ulaska u petlju naziva se invarijanta petlje.

Svaka petlja ima puno invarijanti. Tako je, na primer, x*0=0 invarijanta svake petlje. Međutim, korisna invarijanta je samo ona koja vodi ka pauslovu kada uslov za ulazak u petlju nije ispunjen.

Kako odrediti korisnu invarijantu petlje? Invarijantu petlje je moguće na osnovu nekoliko test primera naslutiti a zatim ju je potrebno formalno dokazati. Drugi način je formalno izvođenje unvarijante. Jedan od načina izvođenja invarijante je uvođenje brojača u petlju što je i urađeno u primeru Hardverdsko celobrojno deljenje.

Formalna verifikacija programa metodom induktivne invarijante zasniva se na dokazu da se iz preduslova može uspostaviti invarijanta pre prvog ulaska u petlju, zatim da svaki put kada se ulazi u petlju važi dati uslov i, na kraju, da pri prestanku važenja uslova ulaska u petlju on vodi ka ostvarivanju pauslova programa.

Dokaz ispravnosti programa metodom induktivne invarijante se, dakle, sastoji iz tri koraka:

  1. Uspostavljanje invarijante
  2. Održavanje invarijante
  3. Ostvarivanje željenog pauslova

Na kraju, da bi se dokazala totalna korektnost programa, treba dokazati i da se program zaustavlja.

Formalni dokazi su interesantni jer mogu da se generišu automatski uz pomoć računara ili barem interaktivno u saradnji čoveka sa računarom. U oba slučaja, formalni dokaz može da se proveri automatski, dok provera neformalnog dokaza nije laka. Takođe, kada se program i njegov dokaz istovremeno razvijaju, programer bolje razume sam program i proces programiranja uopšte. Programeri su zainteresovani za formalne dokaze jer metodologija dokaza utiče na razmatranje preciznosti, konzistentnosti i kompletnsoti specifikacije, na jasnoću implementcije i konzistentnost implementacije i specifikacije. Zahvaljujući tome dobija se pouzdaniji softver, čak i onda kada se formalni dokaz ne izvede eksplicitno.

Za neki program može se dokazati tvrđenje "program kao rezultat vraća faktorijel ulazne vrednosti”. U nekim slučajevima može se dokazati tvrđenje ,,program ima prosečno vreme izvršavanja 0.5 sekundi”. Tvrđenja ,,prosečno vreme između dva pada programa je najmanje 8 sati sa verovatnoćom 95%” i ,,prosečno vreme izvršavanja programa je dobro” ne mogu se formalno dokazati.

Raketa Ariana 5 je eksplodirala 4. juna 1996. godine, samo 40 sekundi nakon lansiranja u orbitu. Do nesreće je došlo zbog greške u softveru. Ta greška koštala je više od pola milijarde dolara, a nastala je usled nepažljivog korišćenja specifikacije pisane za prethodni projekat rakete kao i izostanka verifikacije za novu generaciju. Više o ovome može se pročitati u zvaničnom izveštaju.



Naredna: FaktorijelGore: Uvod Prethodna: Algoritmi, pseudokod i dijagrami toka   Sadržaj