*Pravilnost algoritma

Žal je pri številnih problemih veljavnih vhodov preprosto preveč (ali celo neskončno), zato algoritmov pogosto ne moremo sistematično preveriti. V takih primerih je treba pravilnost algoritma dokazati. Dokažimo pravilnost našega prvega algoritma za problem MIN3:

Pravilnost moramo pokazati za vse trojice vhodnih števil a, b in c. Pričnimo takole: recimo da je število a manjše tako od b kot od c. To pomeni, da velja a < b in hkrati a < c. Za ta primer bi moral biti izhod algoritma enak a. Pa je res? Seveda! Ker po predpostavki velja a < b, je pogoj v prvem pogojnem stavku izpolnjen. Zaradi a < c je pogoj izpolnjen tudi v drugem pogojnem stavku, kar pomeni, da funkcija vrne število a. Na ta način smo zajeli že ogromno možnih vhodov (npr. vhod a = 2, b = 3, c = 4 ali pa vhod a = −50, b = −30, c = −40), ne pa še vseh. Lahko se zgodi, da je število b najmanjše (b < a in b < c). Tudi v tem primeru ni težko preveriti, ali se rezultat funkcije (število b) ujema s pričakovanim izhodom. Preverimo še možnost, da je število c najmanjše (torej c < a in c < b). V tem primeru bi moral biti rezultat funkcije enak c. Drži! Funkcija vrne c tako v primeru, ko je število a manjše od števila b, kot tudi v nasprotnem primeru.

Vaja

Dokaz smo razdelili na tri primere:

a < b in a < c
b < a in b < c
c < a in c < b

Vendar pa s temi primeri nismo zajeli celotne množice veljavnih vhodov, zato naš dokaz še ni povsem končan. Katere primere moramo še obravnavati?

Oglejmo si še dokaz pravilnosti algoritma, ki vsebuje zanko. Naslednja funkcija vrne najmanjše število v podani neprazni tabeli:

Vaja

Preden se lotimo dokaza, izvedi zgornjo funkcijo na papirju, in sicer za tabelo [3, 5, 2, 8, 4, 10, 6]. Kaj vsebuje spremenljivka naj po prvem, drugem, tretjem, ... obhodu zanke? Kaj vsebuje po i-tem obhodu zanke?