Pravilnost programa

Iz MaFiRaWiki

Pri razvoju programov je osnovna zahteva, da je program pravilen, kar pomeni, da za vse pravilne vhodne podatke dobimo v končnem času pravilen rezultat. Pravilnost programov preverjamo na več načinov:

  1. z branjem programa in intuitivnim razumevanjem, kaj program dela
  2. s testiranjem programa na izbrani množici testnih podatkov
  3. s formalnim dokazom pravilnosti programa

Prvi dve metodi sta skoraj vedno nepopolni, saj napako lahko spregledamo na isti način, kot jo je programer. Pri testiranjih programov lahko dokažemo samo napačnost delovanja programa, pravilnost pa dokažemo samo za tiste vhodne podatke, na katerih smo program dejansko izvajali. Tretja metoda je najzahtevnejša, saj zahteva natančno analizo programa in formalen opis pomembnih relacij med podatkovnimi objekti med izvajanjem programa. V praksi to metodo zaradi zahtevnosti bolj redko uporabljamo, kajti dokazi pravilnosti programa so tipično daljši od samega programa in možno je, da se pojavijo napake tudi v dokazu. Formalno dokazovanje uporabimo zaradi naslednjih razlogov:

  • omogoča boljše razumevanje, kaj pravilnost programa dejansko pomeni in razjasni težavnost preverjanja pravilnosti programa
  • za določene algoritme, ki jim intuitivno ni moč zaupati
  • pri kritičnih delih kode, kjer bi napačno delovanje povzročilo katastrofalne posledice, z dokazom pa zagotovimo zanesljivost programske opreme.

Program definiramo kot preslikavo: f:X \to Z,

ki preslika vhodne podatke <x_1, \ldots, x_n> \in X v izhodne podatke <z_1, \ldots, z_m> \in Z.

Pri tem morajo vhodni podatki izpolnjevati začetni pogoj \Phi(x_1, \ldots, x_n).

Izhodni podatki pa morajo izpolnjevati zaključni pogoj: \Psi(z_1, \ldots, z_m, x_1, \ldots, x_n), pri čemer predpostavimo, da se vrednost vhodnih podatkov med izvajanjem programa ne spreminjajo.

Pravimo, da je program:

  • parcialno pravilen, če v primeru, da se za vhodne podatke, ki izpolnjujejo začetni pogoj Φ, ustavi, izhodni podatki izpolnjujejo zaključni pogoj Ψ.
  • totalno pravilen, če je parcialno pravilen, in če za vse vhodne podatke, ki izpolnjujeo začetni pogoj Φ, po končnem številu korakov ustavi.

Viri

  • Igor Kononenko, Marko Robnik Šikonja, Algoritmi in podatkovne strukture II, Fakulteta za računalništvo in informatiko, 2004
Osebna orodja