4 Dokazovanje pravilnosti programov

Kako vemo, ali program deluje pravilno? Kako vemo, kakšen program želimo sestaviti?

Ločimo med specifikacijo in implementacijo programa:

• Specifikacija je opis, kaj naj želeni program počne.

• Implementacija je program, ki počne to, kar zahteva specifikacija.

Specifikacija je lahko podana bolj ali manj natančno, v človeškem jeziku ali zapisana v formalnem matematičnem jeziku. Specifikacije imajo več namenov:

• da pridobimo opis programa, ki naj bi ga sestavili

• da lahko preverimo, ali je implementacija pravilna

• zagotovimo kompatibilnost med različnimi deli programske opreme

Danes bomo spoznali “specifikacije v malem”, s katerimi povemo, kaj naj počne konkreten košček izvorne kode. Kasneje bomo govorili tudi o specifikaciji in implementaciji večjih programskih enot, ki zajemajo zbirko podatkovnih tipov in funkcij.

4.1Hoarova logika¶

V matematiki običajno uporabljamo samo eno zvrst logike, namreč klasično logiko prvega reda. V računalništvu pa je različnih logik veliko, saj ena sama ne zadošča vsem potrebam. Danes bomo spoznali logiko, ki jo je zasnoval britanski računalničar Tony Hoare.

V Hoarovi logiki delovanje programa opišemo s Hoarovimi trojicami

{ P } c { Q }

Tu sta P in Q logični formuli in c ukaz. Formuli P pravimo predpogoj (angl. precondition), formuli Q pravimo končni pogoj (ang. postcondition). Skupaj tvorita specifikacijo, program c pa je implementacija.

Izkaže se, da je pravilnost programa lažje obravnavati v dveh korakih:

1. Ali program deluje pravilno, če se ustavi?

2. Ali se program ustavi?

V ta namen uvedemo dve vrsti Hoarovih trojic:

Zapomnimo si: delna pravilnost ne zagotavlja, da se bo c končal, popolna pravilnost to zagotavlja.

Kaj lahko počnemo s specifikacijami? Če imam dano specifikacijo, lahko poiščemo program, ki ji ustreza.

Hoarove trojice običajno pišemo navpično, takole:

{ x = m ∧ y = n }
c
{ x = min(m, n) ∧ y = max(m, n) }

Če imamo opravka z večimi vrsticami kode, vrivamo predpogoje med vrstice

{ P₁ }
c₁
{ P₂ }
c₂
{ P₃ }
c₃
⋯

in jih beremo kot zaporedje Hoarovih trojic: velja { P₁ } c₁ { P₂ } in velja { P₂ } c₂ { P₃ } in velja { P₃ } c₃ { P₄ } in tako naprej.

4.2Pravila sklepanja¶

Vsaka logika ima svoja pravila sklepanja, s katerimi izpeljujemo dokaze. Za Hoarovo logiko veljajo naslednja pravila sklepanja.

4.2.1Splošna pravila¶

Vedno smemo uporabiti veljavno logično in matematično sklepanje, na primer:

P' ⇒ P    { P } c { Q }      Q ⇒ Q'
——————————————————————————————————–
          { P' } c { Q' }


{ P₁ } c { Q₁ }     { P₂ } c { Q₂ }
——————————————————————————————————–
     { P₁ ∧ P₂ } c { Q₁ ∧ Q₂ }

Naj bodo FV(P) vse spremenljivke, ki se pojavljajo v formuli P (free variables) in FA(c) vse spremenljivke, ki jih c nastavlja (assigned variables). Na primer:

FV(x ≤ y ∨ x > 0) = {x, y}

FA(if x < y then x := y + 3 else skip end) = { x }

Velja pravilo:

FV(P) ∩ FA(c) = ∅
—————————————————
  { P } c { P }

To pravilo pove, da ukaz c ne vpliva na izjavo P, če nimata skupnih spremenljivk. Tako pravilo ne bi veljalo v programskem jeziku s kazalci, saj bo lahko c spreminjal vrednosti, ki so dosegljive iz P, čeprav jih P ne omenja.

4.2.1.1Pravilo za skip¶

Ukaz skip nima nikakršnega učinka na veljavnost izjave:

———————————————–
{ P } skip { P }

4.2.1.2Pravilo za pogojni stavek¶

Pri pogojnem stavku obravnavamo dva primera, enega za then in drugega za else.

{ P ∧ b } c₁ { Q }       { P ∧ ¬b } c₂ { Q }
———————————————————————————————————————————–
    { P } if b then c₁ else c₂ end { Q }

4.2.1.3Pravilo za c₁ ; c₂¶

Pravilo za ; veriži končni pogoj prvega ukaza s predpogojem drugega:

{ P } c₁ { Q }      { Q } c₂ { R }
—————————————————————————————————–
       { P } c₁ ; c₂ { R }

4.2.1.4Pravilo za zanko while¶

        { P ∧ b } c { P }
—————————————————-————————————————–
{ P } while b do c done { ¬ b ∧ P }

Formuli P pravimo invarianta zanke while. Izmed vseh pravil, je tega najtežje uporabljati, ker je treba imeti nekaj izkušenj, da najdemo ustrezni P.

4.2.1.5Pravilo za prirejanje¶

————————————————————————–
{ P[x ↦ e] } x := e { P }

Zapis P[x ↦ e] pomeni “v izjavi P zamenjaj x z e”.

4.2.2Popolna pravilnost¶

Vsa zgornja pravila, razen dveh, lahko predelamo v popolno pravilnost, na primer:

[ P ∧ b ] c₁ [ Q ]       [ P ∧ ¬b ] c₂ [ Q ]
———————————————————————————————————————————–
    [ P ] if b then c₁ else c₂ end [ Q ]

Prva izjema je pravilo

FV(P) ∩ FA(c) = ∅
—————————————————
  { P } c { P }

ki ga predelamo takole

FV(P) ∩ FA(c) = ∅    [ R ] c [ Q ]
——————————————————————————————————
      [ R ∧ P ] c [ Q ∧ P ]

Pri zanki while zagotovimo, da se bo končala, tako da poiščemo količino, ki se zmanjšuje, a se ne more zmanjševati v nedogled. Na primer, to je lahko celoštevilska pozitivna vrednost.

Pravilo za popolno pravilnost while se glasi:

Naj bo e količina, ki se ne more v nedogled zmanjševati (na primer naravno število):

 [ P ∧ b ∧ e = z ] c [P ∧ e < z ]        z ∉ FA(c)
 ————————————————————————————————————————————————
      [ P ] while b do c done [ ¬ b ∧ P ]

V tem pravilu je z duh, kar formalno napišemo kot z ∉ FA(c). Kako pa ta pravila v praksi uporabljamo? Poglejmo nekaj primerov.

4.3Primeri¶