Jedno od centralnih pitanja u razvoju programa je pitanje njegove ispravnosti (korektnosti). Softver je u današnjem svetu prisutan na svakom koraku: softver kontroliše mnogo toga — od bankovnih računa i komponenti televizora i automobila, do nuklearnih elektrana, aviona i svemirskih letelica. U svom tom softveru neminovno su prisutne i greške. Greška u funkcionisanju daljinskog upravljača za televizor može biti tek uznemirujuća, ali greška u funkcionisanju nuklearne elektrane može imati razorne posledice. Najopasnije greške su one koje mogu da dovedu do velikih troškova, ili još gore, do gubitka ljudskih života. Krupne softverske greške i dalje se neprestano javljaju i one koštaju svetsku ekonomiju milijarde dolara. Neki primeri softverskih grešaka koji su izazvali velike probleme opisani su u dodatku 1.A.1.
Postupak pokazivanja da je program ispravan naziva se verifikovanje programa. Međutim, često se pokazuje da pitanje šta uopšte znači da je program ispravan nije uvek očigledno. Na primer, da li je naredna funkcija koja izračunava stepen ispravna?
double stepen(double x, int n) {
double s = 1.0;
for (int i = 0; i < n; i++)
s *= x;
return s;
}Koji je rezultat sledećih poziva stepen(2.0, 10), stepen(-2.0, 10), stepen(2.0,-10), stepen(0.0, 0), stepen(1e200, 2)? Da li su ti rezultati ispravni? Da li je uopšte dozvoljeno da izložilac bude negativan ili da se izračunava \(0^0\)? Da li rezultat \((10^{200})^2\) može uopšte da se ispravno zapiše pomoću tipa double? Sve ovo treba precizirati da bi se uopšte moglo diskutovati da li je ova implementacija stepenovanja ispravna.
Dakle, pre programa potrebno je najpre precizno formulisati pojam ispravnosti programa. Ispravnost programa počiva na pojmu specifikacije. Specifikacija je, intuitivno, opis željenog ponašanja programa koji treba napisati. Specifikacija je obično stvar dogovora između naručioca programa (korisnika) i tima programera koji program razvijaju. Veoma važno je da se pre same implementacije što preciznije dogovori šta je očekivano ponašanje programa. Često se specifikacija menja i precizira tokom razvoja programa.
Specifikacija se obično zadaje u terminima preduslova tj. uslova koje ulazni parametri programa moraju da zadovolje, kao i postuslova tj. uslova koje rezultati izračunavanja moraju da zadovolje. U primeru funkcije stepenovanja preduslov može zahtevati da je vrednost broja \(n \geq 0\) i da ako je \(n=0\), tada je \(x \neq 0\), a postuslov da funkcija vraća vrednost \(x^n\). Kada je poznata specifikacija, potrebno je verifikovati program, tj. dokazati da on zadovoljava specifikaciju. Prikazana implementacija je ispravna u odnosu na ovu specifikaciju samo ako se zanemare problemi preciznosti i opsega zapisa realnih brojeva u računaru.
U okviru verifikacije programa, veoma važno pitanje je pitanje zaustavljanja programa. Parcijalna korektnost podrazumeva da neki program, ukoliko se zaustavi, daje korektan rezultat (tj. rezultat koji zadovoljava specifikaciju). Totalna korektnost podrazumeva da se program za sve (specifikacijom dopuštene) ulaze zaustavlja, kao i da su dobijeni rezultati korektni.
Dva osnovna pristupa verifikaciji su:
dinamička verifikacija koja podrazumeva proveru ispravnosti u fazi izvršavanja programa, najčešće putem testiranja;
statička verifikacija koja podrazumeva analizu izvornog koda programa, često korišćenjem formalnih metoda i matematičkog aparata.
O svakom od njih će biti više reči u nastavku.
Sintaksičke greške u programima su najmanje opasne i najlakše otklonjive, jer ih prijavljuje kompilator i program nije moguće pokrenuti dok se sve sintaksičke greške ne isprave.
Neke greške (na primer, deljenja nulom ili pokušaja pristupa nedozvoljenom delu memorije) mogu dovesti do nasilnog prekida izvršavanja (sintaksički ispravnog) programa (kaže se ponekada da “aplikacija puca”). Mnogo opasnije su logičke greške tj. situacije u kojima se programi uspešno kompilira, pokreće i izvršava ali ne radi ono što je od njega očekivano tj. daje pogrešne rezultate. Greška može biti i u samoj specifikaciji tj. program može da radi tačno ono što je od programera zahtevano, ali to može biti drugačije od onoga što korisnik očekuje ili što je želeo. Veoma važna grupa grešaka su one koje su vezane za bezbednost i sigurnost tj. greške usled kojih zlonamerni korisnici mogu neovlašćeno doći u posed nekih podataka ili resursa.
Navedimo i nekoliko najčešćih uzroka grešaka na nivou implementacije i savete kako da se one zaobiđu.
Greške prekoračenja. Čest razlog grešaka u programima je korišćenje neodgovarajućih tipova podataka, tj. tipova koji uzrokuju da se usled prekoračenja ili potkoračenja dobiju netačni rezultati izračunavanja. Stoga je uvek poželjno imati u vidu moguće raspone vrednosti ulaznih podataka i na osnovu njih proveriti da li su rasponi svih međurezultata i završnih rezultata takvi da mogu da se predstave odabranim tipovima promenljivih. U sklopu provere graničnih vrednosti, poželjno je uvek uključiti i namjanje i najveće moguće vrednosti ulaznih veličina.
Provera graničnih vrednosti. Veliki broj grešaka javlja se na granicama opsega petlje, graničnim indeksima niza, graničnim vrednostima argumenata aritmetičkih operacija i slično. Zbog toga je testiranje na graničnim vrednostima izuzetno važno i program koji prolazi takve ulazne veličine često je ispravan i za druge. Na primer, ako se testira program koji učitava jedan red teksta u neki niz, trebalo bi proveriti da li program ispravno radi kada je na ulazu prazan red (tj. red koji sadrži samo karakter '\n'). Drugom granicom mogu se smatrati ulazni redovi koji su veoma dugi (duži od broja elemenata niza u koji se učitavaju podaci) ili pre čijeg kraja se nalazi kraj toka podataka. Stoga bi trebalo proveriti i da li se program ispravno ponaša pri učitavanju redova koji su dugi koliko i niz u koji se učitavaju podaci ili kraći za jedan karakter, duži za jedan karakter i slično.
Proveravanje pre-uslova. Da bi neko izračunavanje imalo smisla često je potrebno da važe neki pre-uslovi. Na primer, ako je potrebno izračunati prosečan broj poena \(n\) studenata, pitanje je šta raditi ukoliko je \(n\) jednako \(0\) i ponašanje programa treba da bude specifikovano i testirano u takvim situacijama. Moguće je, na primer, da se ako je \(n\) jednako \(0\), vrati \(0\) kao rezultat. Moguće je i da se, ako je \(n\) jednako \(0\), ne dozvoli izračunavanje proseka. U ovom drugom pristupu, pre koda za izračunavanje proseka može da se navede naredba assert(n > 0);, koja u fazi razvoja programa uzrokuje da se prijavi poruka o tome da preduslov zahtevan specifikacijom nije bio ispunjen.
Proveravanje uspešnosti poziva funkcija. Čest izvor grešaka tokom izvršavanja programa je neproveravanje onih povratnih vrednosti funkcija koje ukazuju na to da li je funkcija uspešno uradila ono što što je trebalo. Na primer, funkcije za alokaciju memorije, funkcije za rad sa datotekama itd., naročito ako potiču iz programskog jezika C, kroz svoju povratnu vrednost obaveštavaju programera da li je došlo do neke greške. Povratne vrednosti ovih funkcija ukazuju na potencijalni problem i ukoliko se ignorišu – problem će samo postati veći. Slično, mnoge funkcije u jeziku C++ dovode do izuzetaka ako ne mogu uspešno da izvrše svoj zadatak. Te izuzetke bi trebalo “uhvatiti” i obraditi tj. učiniti ono što je moguće da program nastavi sa radom ili da bar korisniku prijavi jasnu poruku o tome zašto je došlo do greške i zašto je izvršavanje programa moralo biti prekinuto.
Dinamičko verifikovanje programa podrazumeva proveravanje ispravnosti u fazi izvršavanja programa. Najčešći vid dinamičkog verifikovanja programa je testiranje.
Najznačajnija vrsta dinamičkog ispitivanja ispravnosti programa je testiranje. Testiranje može da obezbedi visok stepen pouzdanosti programa, ali najčešće ne može da dokaže da je program u potpunosti korektan.
Neka tvrđenja o programu je moguće testirati, dok neka nije. Na primer, tvrđenja poput “program za ovaj ulaz vraća ovaj izlaz” ili “program ima prosečno vreme izvršavanja pola sekunde” su (u principu) proveriva testovima. Međutim, tvrđenje “prosečno vreme izvršavanja programa je dobro” suviše je neodređeno da bi moglo da bude testirano.
U idealnom slučaju, treba sprovesti iscrpno testiranje rada programa za sve moguće ulazne vrednosti i proveriti da li izlazne vrednosti zadovoljavaju specifikaciju. Međutim, ovakav iscrpan pristup testiranju skoro nikada nije praktično primenljiv. Na primer, iscrpno testiranje korektnosti programa koji sabira dva 32-bitna broja, zahtevalo bi ukupno \(2^{32}\cdot 2^{32}=2^{64}\) različitih testova. Pod pretpostavkom da svaki test traje jednu nanosekundu, iscrpno testiranje bi zahtevalo približno \(1{,}8\cdot 10^{10}\) sekundi što je oko 570 godina. Dakle, testiranjem nije praktično moguće dokazati ispravnost čak ni prilično trivijalnih programa. S druge strane, testiranjem je moguće dokazati da program nije ispravan tj. pronaći greške u programima.
S obzirom na to da iscrpno testiranje nije praktično primenljivo, obično se koristi tehnika testiranja tipičnih ulaza programa kao i specijalnih, karakterističnih ulaznih vrednosti za koje postoji veća verovatnoća da dovedu do neke greške. U slučaju pomenutog programa za sabiranje, tipični slučaj bi se odnosio na testiranje korektnosti sabiranja nekoliko slučajno odabranih parova brojeva, dok bi za specijalne slučajeve mogli biti proglašeni slučajevi kada je neki od sabiraka 0, 1, -1, najmanji negativan broj, najveći pozitivan broj i slično.
Postoje različite metode testiranja, a neke od njih su:
Testiranje zasebnih jedinica (engl. unit testing) U ovoj metodi testiranja, nezavisno se testovima proverava ispravnost zasebnih jedinica koda. “Jedinica” je obično najmanji deo programa koji se može testirati. U proceduralnim jezicima, “jedinica” je obično jedna funkcija. Svaki jedinični test treba da bude nezavisan od ostalih, ali puno jediničnih testova može da bude grupisano u baterije testova, u jednoj ili više funkcija sa ovom namenom. Jedinični testovi treba da proveravaju ponašanje funkcije, za tipične, granične i specijalne slučajeve. Ova metoda veoma je važna u obezbeđivanju veće pouzdanosti kada se mnoge funkcije u programu često menjaju i zavise jedna od drugih. Kad god se promeni željeno ponašanje neke funkcije, potrebno je ažurirati odgovarajuće jedinične testove. Ova metoda veoma je korisna zbog toga što često otkriva trivijalne greške, ali i zbog toga što jedinični testovi predstavljaju svojevrsnu specifikaciju.
Postoje specijalizovani softverski alati i biblioteke koje omogućavaju jednostavno kreiranje i održavanje ovakvih testova. Jedinične testove obično pišu i koriste, u toku razvoja softvera, sami autori programa ili testeri koji imaju pristup kodu.
Regresiono testiranje (engl. regression testing) U ovom pristupu, proveravaju se izmene programa kako bi se utvrdilo da se nova verzija ponaša isto kao stara (na primer, generiše se isti izlaz). Za svaki deo programa implementiraju se testovi koji proveravaju njegovo ponašanje. Pre nego što se napravi nova verzija programa, ona mora da uspešno prođe sve stare testove kako bi se osiguralo da ono što je ranije radilo radi i dalje, tj. da nije narušena ranija funkcionalnost programa.
Regresiono testiranje primenjuje se u okviru samog implementiranja softvera i obično ga sprovode testeri.
Integraciono testiranje (engl. integration testing) Ovaj vid testiranja primenjuje se kada se više programskih modula objedinjuje u jednu celinu i kada je potrebno proveriti kako funkcioniše ta celina i komunikacija između njenih modula. Integraciono testiranje obično se sprovodi nakon što su pojedinačni moduli prošli kroz druge vidove testiranja. Kada nova programska celina, sastavljena od više modula uspešno prođe kroz integraciono testiranje, onda ona može da bude jedna od komponenti celine na višem nivou koja takođe treba da prođe integraciono testiranje.
Testiranje valjanosti (engl. validation testing) Testiranje valjanosti treba da utvrdi da sistem ispunjava zadate zahteve i izvršava funkcije za koje je namenjen. Testiranje valjanosti vrši se na kraju razvojnog procesa, nakon što su uspešno završene druge procedure testiranja i utvrđivanja ispravnosti. Testovi valjanosti koji se sprovode su testovi visokog nivoa koji treba da pokažu da se u obradama koriste odgovarajući podaci i u skladu sa odgovarajućim procedurama, opisanim u specifikaciji programa.
Testiranje, kao jedan od ključnih vidova za osiguranje kvaliteta softvera (eng. quality assurance), se danas razvilo se u dobro utemeljenu i široko podržanu oblast računarstva. Jedan od pravaca unapređivanja procesa testiranja je njegova automatizacija. Umesto da testiranje sprovodi osoba (tester), automatskim testiranjem taj postupak preuzima računar i sprovodi ga automatski i mnogo brže, dok tester može da se posveti dizajnu automatskih testova i analizi rezultata automatskog testiranja.
U savremenim metodologijama za razvoj softvera, testiranje se u proces razvoja uvodi rano i zahteva saradnju programera i testera. Autor automatskih testova realizuje ih korišćenjem namenskih biblioteka i alata (koji mogu, na primer, da simuliraju i komunikaciju korisnika putem grafičkog korisničkog interfejsa). Programer tako automatizovane testove može da koristi u okviru nekih integrisanih razvojnih okruženja. Postoji mnoštvo alata za automatizovano sprovođenje testiranja. Neki od njih deo su integrisanih razvojnih okruženja a neki se koriste kao samostalni sistemi. Oni se razlikuju i po veličini, zahtevanom umeću i po vrsti podrške za timski rad. Na primer, naredni testovi u biblioteci Google test (googletest) se mogu upotrebiti za automatsko testiranje funkcije koja izračunava stepen.
double stepen(double x, int n);
TEST(StepenTest, PozitivanEksponent) {
EXPECT_DOUBLE_EQ(stepen(2.0, 3), 8.0);
}
TEST(StepenTest, NulaEksponent) {
EXPECT_DOUBLE_EQ(stepen(2.0, 0), 1.0);
}
TEST(StepenTest, NegativanEksponent) {
EXPECT_DOUBLE_EQ(stepen(2.0, -1), 0.5);
}Testovi se pokreću automatski i nakon pokretanja prijavljuje se sledeći izveštaj, koji ukazuje na to da funkcija nije korektno implementirana za negativne izložioce.
[==========] Running 3 tests from 1 test suite. [ RUN ] StepenTest.PozitivanEksponent [ OK ] StepenTest.PozitivanEksponent [ RUN ] StepenTest.NulaEksponent [ OK ] StepenTest.NulaEksponent [ RUN ] StepenTest.NegativanEksponent stepen_test.cpp:25: Failure Expected equality of these values: stepen(2.0, -1) Which is: 1 0.5 [ FAILED ] StepenTest.NegativanEksponent [==========] 4 tests ran. [ PASSED ] 3 tests. [ FAILED ] 1 test.
I pored automatizacije, obično ostaje i važan prostor za ručno testiranje, posebno za aspekte korišćenja programa koje nije lako automatizovati (poput subjektivnog osećaja korisnika).
Testiranje je proces provere da li program radi ispravno, odnosno sistematičan pokušaj da se pronađu greške. Debagovanje se koristi onda kada znamo (ili sumnjamo) da greška postoji i želimo da je pronađemo i otklonimo.
Debager je alat koji omogućava praćenje izvršavanja programa korak po korak. Umesto da se program izvrši “odjednom”, debager omogućava programeru da zaustavi izvršavanje na određenim mestima, prati tok programa i ispituje stanje podataka (vrednosti promenljivih, stanje memorije, stanje na pozivnom, programskom steku, itd).
Osnovni pojmovi u radu sa debagerom su:
Posmatranjem ovih informacija programer može da uoči gde dolazi do neočekivanog ponašanja i lakše pronađe uzrok greške.
Da bi se program debagovao, potrebno je kompajlirati ga u debag režimu (npr. u C++-u pomoću opcije -g). Nakon toga se program pokreće u debageru (na primer, gdb ili njegov grafički interfejs kdbg).
Savremena razvojna okruženja, kao što su Visual Studio i Visual Studio Code (Slika 1), imaju ugrađene debagere koji omogućavaju jednostavno postavljanje tačaka prekida, praćenje promenljivih i kontrolu izvršavanja programa, što debagovanje čini znatno jednostavnijim.
Statičko ispitivanje ispravnosti programa, (tj. statička verifikacija) podrazumeva analizu izvornog koda programa (bez njegovog izvršavanja). Takve analize mogu da sprovode i ljudi samostalno (“na papiru”), ali ih obično sprovode ljudi uz pomoć namenskih alata ili namenski programi, potpuno automatski.
Proces verifikacije može biti neformalan i formalan. Neformalnu verifikaciju sprovode programeri, analizom koda, posebno nekih kritičnih delova. Formalna verifikacija zasniva se na precizno definisanoj semantici programskog jezika i strogom logičkom okviru u kojem se dokazi korektnosti izvode. Formalno dokazana ispravnost vodi do najvišeg mogućeg nivoa pouzdanosti programa. Formalno dokazivanje ispravnosti je obično veoma zahtevno, te se ono retko primenjuje, obično samo za bezbednosno kritične programe (kao što je, na primer, program za upravljanje metroom).
Ne postoji algoritam koji za proizvoljan algoritam može da dokaže da zadovoljava svoju specifikaciju (baš kao što ne postoji ni algoritam koji može da ispita da li se proizvoljni program zaustavlja). Najveći problemi u tome su zaustavljanje i analiza petlji. Ono što jeste moguće je postojanje algoritama koji u nekim slučajevima i sa nekim pojednostavljivanjima mogu da dokažu ispravnost zadatog programa.
Potpuno precizna, formalna verifikacija programa zahteva poznavanje svih detalja semantike programskih jezika. Jedan od izazova u tome predstavlja činjenica da se semantika uobičajenih tipova podataka i operacija u programima razlikuje od uobičajene semantike matematičkih operacija nad celim i realnim brojevima (iako velike sličnosti postoje). Na primer, iako tip int podseća na skup celih brojeva, a operacija sabiranja dva podatka tipa int na sabiranje dva cela broja, razlike su evidentne — domen tipa int je konačan (fiksne “širine”), a operacija se vrši “po modulu” tj. u nekim slučajevima dolazi do prekoračenja. Mnoga pravila koja važe za cele brojeve ne važe za podatke tipa int. Na primer, \(x \ge 0 \wedge y \ge 0 \Rightarrow x + y \ge 0\) važi ako su \(x\) i \(y\) celi brojevi, ali ne važi ako su podaci tipa int. U nekim slučajevima, prilikom verifikacije ovakve razlike se apstrahuju i zanemaruju. Time se, naravno, gubi potpuno precizna karakterizacija ponašanja programa i “dokazi” korektnosti prestaju da budu dokazi korektnosti u opštem slučaju. Ipak, ovim se značajno olakšava proces verifikacije i u većini slučajeva ovakve aproksimacije ipak mogu značajno da podignu stepen pouzdanosti programa.
U nastavku teksta, ovakve aproksimacije će biti često vršene. Dakle, u narednom tekstu će fokus biti stavljen na ispitivanje korektnosti algoritama, a ne njihove konkretne implementacije koja zavisi od tehničkih detalja programskog jezika u kom su oni implementirani (na primer, pitanja reprezentacije podataka i prekoračenja).
Ključna ideja u konstrukciji algoritama je to da je konstrukcija algoritama veoma tesno povezana sa dokazivanjem teorema matematičkom indukcijom. Cilj ovog poglavlja (ali i ostatka ove knjige) je da pokažemo da je matematička indukcija osnovni alat za analizu svih vrsta programa (i iterativnih i rekurzivni), ali i više od toga – ona je osnovni alat za konstrukciju algoritama. U tom svetlu se precizna analiza korektnosti nekog algoritma ne vrši nakon što je algoritam konstruisan, već je ona prisutna sve vreme tokom same konstrukcije algoritma. Dokaz teoreme kokreknosti algoritma i sam algoritam su neraskidivo povezani.
Matematička indukcija, u svom osnovnom obliku, je sledeći način dokazivanja osobina prirodnih brojeva. Neka je \(P\) proizvoljno svojstvo koje se može formulisati za prirodne brojeve. Tada važi
\[(P(0) \wedge (\forall n)(P(n) \Rightarrow P(n+1))) \Rightarrow (\forall n)(P(n))\]
Dakle, da bismo dokazali da svaki prirodan broj ima neko svojstvo \(P\) (tj. da bismo dokazali \((\forall n)(P(n))\)), dovoljno je da dokažemo da nula ima to svojstvo (tj. \(P(0)\)) i da dokažemo da čim neki broj ima to svojstvo, ima ga i njegov sledbenik (tj. da dokažemo \((\forall n)(P(n) \Rightarrow P(n+1))\)). Prvo tvrđenje se naziva baza indukcije, a drugo induktivni korak. Prinicip matematičke indukcije je prilično jasan – na osnovu baze znamo da 0 ima svojstvo \(P\), na osnovu koraka da njen sledbenik tj. 1 ima svojstvo \(P\), na osnovu koraka da njegov sledbenik tj. 2 ima svojstvo \(P\) itd. Intuitivno nam je jasno da na ovaj način možemo stići do bilo kog prirodnog broja, koji sigurno mora imati svojstvo \(P\). Baza se može formulisati i za veće vrednosti od nule, ali onda možemo da tvrdimo samo da elementi koji su veći ili jednaki od baze imaju svojstvo \(P\).
Osnovni pristup konstrukcije algoritama je tzv. induktivni tj. rekurzivni pristup. U ovom pristupu cilj je od rešenja problema zadatog oblika ali manje dimenzije dobiti rešenje tog problema veće dimenzije (u naprednijim oblicima je moguće i da se rešava veći broj problema manje dimenzije). Pritom, za početne dimenzije problema (koje zovemo bazni slučajevi) rešenje mora da se izračuna neposredno, bez daljeg svođenja na probleme manje dimenzije. Ako se prilikom svođenja dimenzija problema uvek smanjuje, konstruisani algoritmi će se uvek zaustavljati (jer dimenzija mora da bude nenegativna).
Implementacija algoritma može biti takva da promenljive unutar petlje iterativno ažuriraju svoje vrednosti krenuvši od vrednosti za bazne slučajeve, pa do krajnjih vrednosti koje predstavljaju rešenja zadatog problema. Pošto je ovo prilično slično principu matematičke indukcije, kažemo da je algoritam definisan induktivno.
Implementacija može biti takva da funkcija koja rešava polazni problem samu sebe poziva da bi rešila problem istog oblika, ali manje dimenzije (osim u baznim slučajevima, koji se neposredno rešavaju) i tada kažemo da je algoritam definisan rekurzivno.
Induktivna konstrukcija leži u osnovni praktično svih iterativnih algoritama koje smo do sada razmatrali. Na primer, prikazani algoritam stepenovanja počiva na tome da znamo da izračunamo nulti stepen broja (to je 1) i da ako znamo da izračunamo \(x^k\), tada umemo da izračunamo i \(x^{k+1}\) (to radimo tako što taj poznati stepen \(x^k\) pomnožimo sa \(x\)).
double stepen(double x, int n) {
double s = 1.0;
for (int i = 0; i < n; i++)
s = s * x;
return s;
}Dakle, i u ovom algoritmu imamo induktivnu bazu (koja odgovara inicijalizaciji promenljive pre ulaska u petlju) i induktivni korak (koji odgovara telu petlje, u kom se ažurira vrednost rezultujuće promenljive, u ovom slučaju stepena). Baza može odgovarati i slučaju prvog (a ne obavezno nultog) stepena, ali tada ne možemo da garantujemo da će algoritam ispravno izračunavati nulti stepen.
Rekurzivna implementacija izračunavanja stepena može biti sledeća (u njoj se prilikom rešavanja problema dimenzije \(n > 0\) eksplicitno zahteva rešavanje problema dimenzije \(n-1\)).
double stepen(double x, int n) {
if (n == 0)
return 1.0;
else
return stepen(x, n-1) * x;
}Definisanje algoritama induktivno-rekurzivom konstrukcijom je u veoma tesnoj vezi sa dokazivanjem njihove korektnosti. Iako postoje formalni okviri za dokazivanje korektnosti imperativnih programa (pre svega Horova logika), u ovom poglavlju ćemo se baviti isključivo neformalnim dokazima i veza između logike u kojoj vršimo dokazivanje i (imperativnog) programskog jezika u kojem se program izražava biće prilično neformalna.
Kao što smo već nagovestili, prilikom dokazivanja korektnosti programa obično ćemo ignorisati ograničenja zapisa brojeva u računaru i podrazumevaćemo da je opseg brojeva neograničen i da se realni brojevi zapisuju sa maksimalnom preciznošću. Dakle, obično ćemo ignorisati greške koje mogu nastati usled prekoračenja ili potkoračenja vrednosti tokom izvođenja aritmetičkih operacija. Ipak, prekoračenja ili potkoračenja mogu biti uzrok bitnih grešaka u nekim programima i tada u ispitivanju ispravnosti koristimo bogatije modelovanje zapisa brojeva.
U principu, dokazivanje korektnosti najjednostavnije je za programe koji su sačinjeni od rekurzivno definisanih funkcija koje ne koriste elemente imperativnog programiranja (kao što su dodele vrednosti promenljivama, petlje i slično). Takve programe zovemo funkcionalni programi. Glavni razlog za jednostavnije dokazivanje ispravnosti ovakvih programa je to što se njihove funkcije mogu jednostavno modelovati matematičkim funkcijama (koje za iste argumente uvek daju iste vrednosti). Naime, u funkcionalnim programima funkcije za iste ulazne argumente takođe uvek vraćaju istu vrednost. To je tako zbog pretpostavke da nema eksplicitne dodele vrednosti promenljivama, kao i da kontekst poziva i globalne promenljive ne utiču na izvršavanje funkcija. Dokazivanje korektnosti rekurzivnih funkcija teče nekim oblikom matematičke indukcije.
Problem: Definisati funkciju koja za dati prirodan broj \(n \geq 0\) i dat realan broj \(x\) (različit od \(0\) ako je \(n=0\)) izračunava \(x^n\).
Kao što smo videli, algoritam se veoma jednostavno konstruiše induktivno-rekurzivnom konstrukcijom. Dimenzija problema u ovom primeru je izložilac \(n\).
Rekurzivna implementacija, kao što smo videli je sledeća.
double stepen(double x, int n) {
if (n == 0)
return 1.0;
else
return stepen(x, n-1) * x;
}Korektnost se može formulisati u obliku sledeće teoreme (koju dokazujemo zanemarujući pitanja reprezentacije brojeva u računaru).
Teorema 1.4.1. Za svaki prirodan broj \(n\geq 0\) i realan broj \(x\) (različit od 0, ako je \(n=0\)), rekurzivna funkcija stepen vraća vrednost \(x^n\) tj. važi \(\mathit{stepen}(x, n) = x^n\).
Dokaz. Teoremu možemo dokazati indukcijom.
Bazu indukcije predstavlja slučaj \(n=0\), tj. poziv stepen(x, 0). Na osnovu definicije funkcije stepen rezultat je \(1\), što je ujedno i vrednost \(x^0\) (jer je po specifikaciji tada \(x \neq 0\)).
Induktivna hipoteza je tvrđenje: poziv stepen(x, n-1) vraća vrednost \(x^{n-1}\). Iz te pretpostavke potrebno je da dokažemo da poziv stepen(x, n) vraća vrednost \(x^n\). Na osnovu definicije funkcije stepen, poziv stepen(x, n) će vratiti proizvod stepen(x, n-1) * x. Na osnovu induktivne hipoteze znamo da poziv stepen(x, n-1) vraća \(x^{n-1}\), pa je stoga rezultat \(x^{n-1} \cdot x\), što je upravo \(x^n\). \(\Box\)
Primećujemo ogromnu sličnost između rekurzivne konstrukcije algoritma i induktivnog dokaza njegove korektnosti. Stoga slobodno možemo da kažemo da su rekurzija i indukcija “dve strane iste medalje” (indukciju koristimo kao tehniku dokazivanja, a rekurziju kao tehniku definisanja funkcija tj. konstrukcije algoritama).
Primetimo i da ovaj oblik korišćenja matematičke indukcije nije onaj uobičejeni, jer se ne koristi indukcija neposredno po prirodnim brojevima, već se koristi indukcija po strukturi rekurzivne funkcije u kojoj se, iz pretpostavke da svaki rekurzivni poziv vraća korektan rezultat, dokazuje da funkcija vraća korektan rezultat. Takva forma matematičke indukcije se može dokazati na osnovu uobičajene indukcije po broju rekurzivnih poziva, pod pretpostavkom da se dokaže da se rekurzivna funkcija uvek zaustavlja.
Isti problem stepenovanja se može rešiti i na sledeći način, efikasnije. Ovaj algoritam poznat je pod nazivom brzo stepenovanje. Na primer, umesto da \(2^{10}\) izračunavamo kao \(2^9 \cdot 2\), brže ga možemo izračunati kao \((2^2)^5\). Rekurzivna definicija tada izgleda ovako.
\[ x^n = \begin{cases} 1 & \text{ako } n = 0, \\ (x^2)^{n/2} & \text{ako je } n \text{ paran,} \\ x \cdot x^{n-1} & \text{ako je } n \text{ neparan.} \end{cases} \]
float stepen_brzo(float x, unsigned n)
{
if (n == 0)
return 1.0f;
else if (n % 2 == 0)
return stepen_brzo(x * x, n / 2);
else
return x * stepen_brzo(x, n - 1);
}Vrednost \(2^{10}\) se ovom funkcijom izračunava na sledeći način (označimo, kratkoće radi, funkciju stepen_brzo sa \(s\)):
\[\begin{eqnarray*} s(2, 10) &=& s(4, 5) = 4 \cdot s(4, 4) = 4 \cdot s(16, 2) = 4 \cdot s(256, 1) =\\ &=& 4 \cdot 256 \cdot s(256, 0) = 4 \cdot 256 \cdot 1 = 1024. \end{eqnarray*}\]
Teorema 1.4.2. Za svaki prirodan broj \(n\geq 0\) i realan broj \(x\) (različit od 0, ako je \(n=0\)), rekurzivna funkcija stepen_brzo vraća vrednost \(x^n\) tj. važi \(\mathit{stepen\_brzo}(x, n) = x^n\).
Dokaz. Dokažimo ispravnost navedene funkcije. Kako je u ovom slučaju funkcija definisana opštom rekurzijom, dokaz će pratiti sledeću shemu: “Da bi se pokazalo da vrednost \(\mathit{stepen\_brzo}(x, n)\) zadovoljava neko svojstvo, može se pretpostaviti da za \(n > 0\) i \(n\) parno vrednost \(\mathit{stepen\_brzo}(x \cdot x, n / 2)\) zadovoljava to svojstvo, kao i da za \(n > 0\) i \(n\) neparno vrednost \(\mathit{stepen\_brzo}(x, n-1)\) zadovoljava to svojstvo, i onda tvrđenje treba dokazati pod tim pretpostavkama”. Slične sheme indukcije se mogu dokazati i za druge funkcije definisane opštom rekurzijom i, u principu, one dozvoljavaju da se prilikom dokazivanja korektnosti dodatno pretpostavi da svaki rekurzivni poziv vraća korektan rezultat.1
Pređimo na sâm dokaz činjenice da je \(\mathit{stepen\_brzo}(x, n) = x^n\) (za nenegativnu vrednost \(n\)).
Slučaj \(n = 0\): Tada je \(\mathit{stepen\_brzo}(x, n) = \mathit{stepen\_brzo}(x, 0) = 1 = x^0\).
Slučaj \(n > 0\): Tada je \(n\) ili paran ili neparan.
Slučaj \(n\) je paran: Tada je \(\mathit{stepen\_brzo}(x, n) = \mathit{stepen\_brzo}(x\cdot x, n/2)\). Na osnovu prvog dela induktivne pretpostavke, \(\mathit{stepen\_brzo}(x\cdot x, n/2)\) \(= (x\cdot x)^{n/2}\). Dalje, elementarnim aritmetičkim transformacijama sledi da je \(\mathit{stepen\_brzo}(x, n) = (x\cdot x)^{n/2} = (x^2)^{n/2} = x^n\).
Slučaj \(n\) je neparan: Tada je \(\mathit{stepen\_brzo}(x, n) = x \cdot \mathit{stepen\_brzo}(x,n-1)\). Na osnovu drugog dela induktivne pretpostavke, \(\mathit{stepen\_brzo}(x,n-1)\) \(= x^{n-1}\). Dalje, elementarnim aritmetičkim transformacijama sledi da je \(\mathit{stepen\_brzo}(x, n) = x\cdot x^{n-1} = x^n\). \(\Box\)
U slučaju imperativnih programa (programa koji sadrže naredbu dodele i petlje), aparat koji se koristi za dokazivanje korektnosti mora biti znatno složeniji. Semantiku imperativnih konstrukata znatno je teže opisati u odnosu na (jednostavnu jednakosnu) semantiku čisto funkcionalnih programa. Sve vreme dokazivanja mora se imati u vidu tekući kontekst tj. stanje programa koje obuhvata tekuće vrednosti svih promenljivih koje se javljaju u programu. Program implicitno predstavlja relaciju prelaska između stanja i dokazivanje korektnosti zahteva dokazivanje da će program na kraju stići u neko stanje u kojem su zadovoljeni uslovi zadati specifikacijom. Dodatnu otežavajuću okolnost čine propratni efekti dodela, kao i činjenica da pozivi funkcija mogu da vrate različite vrednosti za iste prosleđene ulazne parametre (u zavisnosti od globalnog konteksta tj. stanja u kojem se poziv izvršio). Zbog toga je dokaz korektnosti složenog programa teže razložiti na elementarne dokaze korektnosti pojedinih funkcija.
Kao najkompleksniji programski konstrukt, petlje predstavljaju jedan od najvećih izazova u verifikaciji. Umesto pojedinačnog razmatranja svakog stanja kroz koje se prolazi prilikom izvršavanja petlje, obično se formulišu uslovi (invarijante petlji) koji precizno karakterišu taj skup stanja. Invarijanta petlje je logička formula koja uključuje vrednosti promenljivih koje se javljaju u nekoj petlji i koja važi pri svakom ispitivanju uslova petlje (tj. neposredno pre, nakon svakog izvršavanja tela petlje, kao i neposredno nakon izvršavanja petlje). Invarijante suštinski opisuju značenje svih promenljivih unutar petlje. Ilustrujmo pojam invarijante na primeru iterativne funkcije za izračunavanje stepena.
double stepen(double x, int n) {
double s = 1.0;
for (int i = 0; i < n; i++)
s = s * x;
return s;
}
int main() {
cout << stepen(2.0, 10) << endl;
}Suština dokaza korektnosti leži u sledećem razmatranju. Nakon inicijalizacije promenljiva \(s\) sadrži vrednost \(1 = x^0 = x^i\). U svakom koraku petlje promenljiva \(s\) se množi sa \(x\), a vrednost \(i\) uvećava za 1, pa i dalje važi \(s=x^i\). Dakle, uslov \(s=x^i\) važi i pre, i tokom i nakon izvršavanja petlje. Pošto je nakon izvršavanja petlje \(i=n\), na kraju promenljiva \(s\) sadrži vrednost \(x^n\), pa, pošto je ta vrednost povratna vrednost funkcije, funkcija ispravno izračunava \(x^n\).
Ovu skicu dokaza možemo dodatno precizirati i dokazati je matematičkom indukcijom.
Teorema 1.4.3. U svakom koraku petlje (i na njenom početku, neposredno nakon provere uslova, ali i na njenom kraju, neposredno nakon izvršavanja tela), kao i nakon izvršavanja cele petlje važi da je \(0 \leq i \leq n\) i da je \(s = x^i\) (gde je \(i\) tekuća vrednost promenljive i, a \(s\) tekuća vrednost promenljive s).
Dokaz. Ovo tvrđenje možemo dokazati indukcijom i to po broju izvršavanja tela petlje (obeležimo taj broj sa \(k\)). Napomenimo samo da ćemo petlju for smatrati samo skraćenicom za petlju while, tako da ćemo inicijalizaciju petlje smatrati za kôd koji se izvršava pre petlje, dok ćemo korak petlje smatrati kao poslednju naredbu tela petlje.
double s = 1.0;
int i = 0;
while (i < n) {
s = s * x;
i++;
}Obeležimo sa \(s_0, s_1, \ldots, s_k, \ldots\) vrednosti promenljive s, a sa \(i_0, i_1, \ldots, i_k, \ldots\) vrednost promenljive i nakon \(0, 1, \ldots, k, \ldots\) izvršavanja tela petlje. Pošto promenljiva n ne menja svoju vrednost, njenu vrednost ćemo označiti sa \(n\).
Bazu indukcije čini slučaj \(k=0\) tj. slučaj kada se telo petlje nije još izvršilo. Pre ulaska u petlju promenljiva i se inicijalizuje na \(0\) (važi \(i_0 = 0\)). Pošto je \(n \geq 0\), važi \(0 \leq i = i_0 = 0 \leq n\). Promenljiva s se inicijalizuje na vrednost \(1\) (važi \(s_0 = 1\)), pa je zaista \(s_0=x^{i_0}\). Dakle, uslovi teoreme su zadovoljeni pre prvog izvršavanja tela petlje.
Pretpostavimo sada kao induktivnu hipotezu da tvrđenje važi nakon \(k\) izvršavanja tela petlje. Dakle, pretpostavljamo da uslovi važe za vrednosti \(s_k\) i \(i_k\) (sa \(s_k\) i \(i_k\) obeležavamo vrednosti promenljivih nakon \(k\) izvršavanja tela petlje) tj. da je \(0 \leq i_k \leq n\) i da je \(s_k = x^{i_k}\). Ako je uslov petlje ispunjen, to će ujedno biti i vrednosti promenljivih na početku tela petlje, pre njenog \(k+1\)-vog izvršavanja.
Iz induktivne hipoteze i pretpostavke da je uslov petlje i < n ispunjen (tj. da je \(i_k < n\)) dokažimo da nakon \(k+1\) izvršavanja tela petlje uslovi teoreme važe i za vrednosti \(s_{k+1}\) i \(s_{k+1}\) (sa \(s_{k+1}\) i \(i_{k+1}\) obeležavamo vrednosti promenljivih nakon \(k+1\) izvršavanja tela petlje). Vrednosti \(s_{k+1}\) i \(i_{k+1}\) se mogu lako odrediti na osnovu vrednosti \(s_k\) i \(i_k\), analizom jednog izvršavanja tela petlje. Na osnovu definicije funkcije važi da je \(s_{k+1} = s_k \cdot x\) i \(i_{k+1} = i_k + 1\). Zato, pošto je \(0 \leq i_k < n\), važi i da je \(0 \leq i_{k+1} \leq n\), pa je uslov koji se odnosi na raspon vrednosti promenljive i očuvan. Na osnovu induktivne hipoteze znamo da je \(s_k = x^{i_k}\). Zato je \(s_{k+1} =x^{i_k} \cdot x = x^{i_k+1} = x^{i_{k+1}}\).
Neka su \(i\) i \(s\) vrednosti promenljivih i i s nakon izvršavanja petlje. Na osnovu dokazanog tvrđenja znamo da uslovi navedeni u njemu važe i nakon završetka petlje. Kada se petlja završi, važi da je \(i = n\) (jer na osnovu prvog uslova znamo da je \(0 \leq i \leq n\), a uslov petlje i < n nije ispunjen). Na osnovu drugog uslova znamo da je \(s=x^i=x^n\).
Zaustavljanje se dokazuje jednostavno tako što se dokaže da se u svakom koraku petlje nenegativna vrednost \(n-i\) smanjuje za po 1, dok ne postane 0. \(\Box\)
Ako razmotrimo strukturu prethodnog razmatranja, možemo ustanoviti da smo identifikovali logičke uslove koji su ispunjeni neposredno pre i neposredno nakon svakog izvršavanja tela petlje. Takvi uslovi se nazivaju invarijante petlje. Da bismo dokazali da je neki uslov invarijanta petlje, dovoljno je da dokažemo:
da taj uslov važi pre prvog ulaska u petlju i
da iz pretpostavke da taj uslov važi pre nekog izvršavanja tela petlje i da je uslov petlje ispunjen dokažemo da taj uslov važi i nakon izvršavanja tela petlje.
Te dve činjenice nam, na osnovu induktivnog argumenta, garantuju da će uslov biti ispunjen pre i posle svake iteracije petlje, kao i nakon izvršavanja cele petlje (ako se ona ikada zaustavi), tj. da će taj uslov biti invarijanta petlje (taj dokaz se može sprovesti klasičnom matematičkom indukcijom na osnovu broja izvršavanja tela petlje). Primetimo da prvi korak odgovara dokazivanju baze indukcije, a drugi dokazivanju induktivnog koraka.
Svaka petlja ima puno invarijanti, pri čemu su neki uslovi “preslabi” a neki “prejaki” tj. ne objašnjavaju ponašanje programa. Na primer, bilo koja valjana formula (na primer, \(x \cdot 0 = 0\) ili \((x \geq y) \vee (y \geq x)\)) je uvek invarijanta petlje. Od interesa su nam samo one invarijante koje u kombinaciji sa uslovom prekida petlje (pod pretpostavkom da petlja nije prekinuta naredbom break) impliciraju uslov koji nam je potreban nakon petlje. Ako je petlja jedina u nekom algoritmu, obično je to onda uslov korektnosti samog algoritma. Dakle, nakon dokaza leme koja čini osnovu dokaza da je neki uslov invarijanta petlje, potrebno je da dokažemo i
Dakle, opšta struktura analize programa korišćenjem invarijanti se može opisati na sledeći način.
<incijalizacija>
// ovde vazi <invarijanta>
while (<uslov>)
// ovde vaze i <uslov> i <invarijanta>
<telo>
// ovde vazi <invarijanta>
// ovde ne vazi <uslov>, a vazi <invarijanta>Prikažimo sada kraću verziju prethodnog dokaza korektnosti funkcije stepenovanja, u kom ćemo koristiti pojam invarijante i nećemo se direktno pozivati na matematičku indukciju.
Lema 1.4.1. Za svaki prirodni broj \(n \geq 0\) i realni broj \(x\) (različit od \(0\) kada je \(n=0\)), u svakom koraku petlje važi da je \(0 \leq i \leq n\) i \(s = x^i\) (ovo je jedna invarijanta petlje).
Dokaz. Dokažimo da je uslov invarijanta.
Pokažimo da invarijanta važi pre ulaska u petlju. Pre ulaska u petlju promenljive imaju vrednosti \(s = 1\) i \(i = 0\), te invarijanta, trivijalno, važi.
Pokažimo da invarijanta ostaje održana nakon svakog izvršavanja tela petlje. Obeležimo sa \(s'\) i \(s''\) i sa \(i'\) i \(i''\) vrednosti promenljivih s i i pre i posle izvršavanja tela i koraka petlje. Pošto se promenljive x i n ne menjaju, njihove vrednosti obeležimo sa \(x\) i \(n\).
Pretpostavimo da invarijanta važi pri ulasku u petlju tj. da važi \(s' = x^{i'}\) i \(0 \leq i' \leq n\). Pošto je uslov petlje ispunjen, važi i \(i' < n\).
Nakon izvršavanja tela petlje, promenljive imaju vrednosti \(s'' = s' \cdot x\) i \(i'' = i' + 1\). Potrebno je pokazati da ove nove vrednosti zadovoljavaju invarijantu, tj. da važi \(s'' = x^{i''}\) i \(0 \leq i'' \leq n\). Zaista, \(s' \cdot x = x^{i'+1}\) što je tačno na osnovu pretpostavke. Takođe, pošto važi da je \(0 \leq i' < n\), važi i da je \(0 \leq i'' \leq n\).
Dakle, ako su \(s\), \(i\), \(n\) i \(x\) tekuće vrednosti promenljivih, tada su \(s = x^i\) i \(0 \leq i \leq n\) invarijante petlje.
\(\Box\)
Pokažimo da dokazana invarijanta obezbeđuje korektnost.
Teorema 1.4.4. Na kraju izvršavanja algoritma važi da je \(s = x^n\).
Dokaz. Kada se izađe iz petlje, važi \(i=n\). Zaista, na osnovu leme znamo da važi invarijanta \(0 \leq i \leq n\), pa pošto ne važi uslov petlje \(i < n\), po izlasku iz petlje mora da važi da je \(i = n\). Kombinovanjem sa invarijantom \(x = s^i\), dobija se da tada važi \(s = x^n\), što je i trebalo dokazati. \(\Box\)
Dokažimo sada korektnost naredne iterativne implementacije algoritma brzog stepenovanja. Ovakvu implementaciju dobijamo prateći promenu promenljivih tokom izvršavanja rekurzivnih poziva. Novouvedena promenljiva \(s\) akumulira konačnu vrednost stepena.
double stepen_brzo(double x, int n) {
double s = 1.0;
while (n > 0) {
if (n % 2 == 1) {
s *= x;
n--;
} else {
x = x * x;
n /= 2;
}
}
return s;
}Razmotrimo kako se menjaju vrednosti promenljivih dok se izračunava stepen \(2^{10}\).
| \(x\) | \(n\) | \(s\) |
|---|---|---|
| 2 | 10 | 1 |
| 4 | 5 | 1 |
| 4 | 4 | 4 |
| 16 | 2 | 4 |
| 256 | 1 | 4 |
| 256 | 0 | 1024 |
Ili malo opštije, ako je inicijalna vrednost promenljive \(x\) jednaka nekoj vrednosti \(c\).
| \(x\) | \(n\) | \(s\) |
|---|---|---|
| \(c\) | 10 | \(1\) |
| \(c^2\) | 5 | \(1\) |
| \(c^2\) | 4 | \(c^2\) |
| \(c^4\) | 2 | \(c^2\) |
| \(c^8\) | 1 | \(c^2\) |
| \(c^8\) | 0 | \(c^{10}\) |
Lema 1.4.2. Neka je \(n \geq 0\) i \(x \neq 0\) ako je \(n = 0\). Neka je \(n_0\) početna vrednost promenljive \(n\), a \(x_0\) promenljive \(x\). Tokom izvršavanja petlje važi invarijanta da je \(n \geq 0\) i \(s \cdot x^n = x_0^{n_0}\).
Dokaz. Razmotrimo inicijalizaciju i održanje invarijante.
Nakon inicijalizacije važi da je \(x=x_0\), \(n=n_0\) i \(s=1\), pa invarijanta trivijalno važi.
Pretpostavimo da invarijanta važi pri ulasku u telo petlje tj. da je \(s \cdot x^n = x_0^{n_0}\). Tada važi i uslov petlje \(n > 0\).
Ako je \(n\) neparan broj, tada je \(n' = n-1\), \(s' = s \cdot x\) i \(x'=x\) pa je \(s' \cdot {x'}^{n'} = s \cdot x \cdot x^{n-1} = s \cdot x^n = x_0^{n_0}\). Pošto je \(n > 0\), važi da je \(n' \geq 0\).
Ako je \(n\) paran broj, tada je \(n' = n / 2\), \(x' = x^2\) i \(s' = s\). Tada je \(s' \cdot {x'}^{n'} = s \cdot (x^2)^{n/2} = s\cdot x^n = x_0^{n_0}\). Pošto je \(n > 0\), važi da je \(n' \geq 0\).
\(\Box\)
Iz ove invarijante sledi korektnost.
Teorema 1.4.5. Neka je \(n \geq 0\) i \(x \neq 0\) ako je \(n = 0\). Tada je \(\mathit{stepen\_brzo}(x, n) = x^n\).
Dokaz. Kada se petlja završi važi invarijanta \(n \geq 0\), \(s \cdot x^n = x_0^{n_0}\), a uslov petlje \(n > 0\) nije ispunjen. Zato je \(n = 0\), pa važi \(s \cdot x^0 = x_0^{n_0}\) tj. \(s = x_0^{n_0}\). Dakle, povratna vrednost funkcije sadržana u promenljivoj \(s\) je upravo jednaka stepenu \(x^n\), za zadate početne vrednosti promenljivih \(x\) i \(n\). \(\Box\)
Za vežbu pokažite i da je naredna, malo jednostavnija implementacija takođe korektna.
double stepen_brzo(double x, int n) {
double s = 1.0;
while (n > 0) {
if (n % 2 == 1)
s *= x;
x *= x;
n /= 2;
}
return s;
}Još nekoliko primera ovako preciznih dokaza korektnosti dato je u dodatku 1.A.2. U nastavku ovog poglavlja videćemo još nekoliko primera primene tehnike invarijante petlje. Mora se priznati da kada se tehnika koristi potpuno formalno, da bi se dokazala korektnost već napisanog programskog koda, to ne deluje naročito inspirišuće (pogotovo, ako su programi jednostavni i ako je jednostavno intuitivno razumeti razloge njihove korektnosti). Retko kada se u praktičnom programiranju korektnost zaista dokazuje potpuno formalno (osim u slučaju softvera koji može da ugrozi veliki broj života, poput, na primer, softvera koji upravlja metro-sistemom u Parizu, koji jeste u potpunosti formalno verifikovan). Međutim, argumente i invarijante na kojima korektnost počiva programer često “provrti po glavi”. Videćemo i da se tehnika invarijanti može upotrebiti i pre nego što je program napisan u cilju izvođenja programskog koda iz specifikacije. Jasne invarijante često jednoznačno ukazuju na to kako programski kôd treba da izgleda i na taj način pomažu u procesu programiranja.
Napisati program koji učitava niz celih brojeva a zatim ga transformiše tako da elementi budu podeljeni u tri dela u zavisnosti od zadatih vrednosti \(A\) i \(B\). U prvom delu su elementi manji od zadate vrednosti \(A\) (vrednosti iz intervala \([-\infty, A)\)), u drugom elementi veći ili jednaki zadatoj vrednosti \(A\) i manji ili jednaki zadatoj vrednosti \(B\) (vrednosti iz intervala \([A, B]\)), a u trećem elementi veći od zadate vrednosti \(B\) (vrednosti iz intervala \((B, +\infty)\)). Nije bitno u kom se redosledu nalaze elementi unutar delova. Učitati elemente u niz, a zatim reorganizovati redosled elemenata u tom nizu (ne koristiti pomoćne nizove).
U jednoj liniji standardnog ulaza nalazi se broj elemenata niza, \(N\), a zatim se, u narednoj liniji nalaze elementi niza razdvojeni razmacima. U poslednje dve linije se nalaze celi brojevi \(A\) i \(B\) odvojeni prazninom, i pri tome je \(A < B\).
Ispisati elemente rezultujućeg niza na standardni izlaz (moguće je ispisati elemente svake od tri grupe u posebnom redu, razdvojene razmacima, a moguće je ispisati i ceo niz u jednom redu ili u više redova).
10 1 3 5 4 8 5 7 2 3 6 3 5
1 2 5 4 3 5 3 7 6 8
Jedan pristup je da se do rešenja dođe u dve faze. U prvoj fazi bi se na početak niza doveli svi elementi koji su manji od broja \(A\), a iza njih bi se postavili svi elementi koji su veći ili jednaki broju \(A\). Nakon toga, u drugoj fazi obrađuje se samo deo niza, i on se ponovo istim postupkom deli na elemente koji su manji ili jednaki od broja \(B\) (to će biti tačno elementi iz intervala \([A, B]\)) i elemente koji su veći od \(B\). Podelu možemo realizovati zasebnom funkcijom, koja prima deo niza koji se reorganizuje i granicu na osnovu koje se vrši podela, a koja vraća poziciju na kojoj počinje drugi deo reorganizovanog niza.
Zadatak možemo rešiti pomoću samo jednog prolaza kroz niz i to “u mestu” tj. bez korišćenja pomoćnog niza. Algoritam u nastavku poznat je pod nazivom “Holandska zastava trobojka” (engl. Dutch national flag, slika 2) i pripisuje se čuvenom informatičaru Dajkstri (engl. Edsger W. Dijkstra).
Održavaćemo tri promenljive l, d i i i tokom petlje nametnućemo sledeće uslove koji će biti invarijante petlje. Pretpostavavićemo da tekuće vrednosti \(l\), \(d\) i \(i\) ovih promenljivih zadovoljavaju \(0 \leq l \leq i \leq d \leq n\) i da važi:
Dakle, održavamo raspored <<<<===???>>>, gde su sa < obeleženi elementi prve grupe, sa = elementi druge, sa ? elementi treće grupe, a sa > elementi četvrte grupe.
Da bi invarijanta važila pre ulaska u petlju, jasno je da mora da važi da je \(i = 0\) i \(d=n\) (jer su svi elementi iz intervala \([i, d) = [0, n)\) neispitani). Takođe, da bismo bili sigurni da su u intervalu \([0, l)\) svi elementi manji od \(A\), taj interval mora biti prazan i mora da važi da je \(l=0\). Nakon ovakve inicijalizacije i interval \([l, i) = [0, 0)\) i interval \([d, n) = [n, n)\) je prazan, pa zadovoljava nametnuti uslov.
Petlja će se izvršavati dok god ima neispitanih elemenata, a to je dok je \(i < d\). Razmotrimo kako treba da izgleda telo petlje, da bi uslovi bili održani.
Na kraju petlje važi da je \(i=d\). Uz ostale nametnute uslove tvrđenje odatle sledi (elementi iz intervala pozicija \([0, l)\) su manji od \(A\), elementi iz intervala pozicija \([l, i) = [l, d)\) su između \(A\) i \(B\), interval nepregledanih elemenata \([i, d)\) je prazan, dok su elementi iz intervala \([d, n)\) veći od \(B\)). Dakle, niz je razbijen na nadovezane segmente \([0, l)\), \([l, d)\) i \([d, n)\) i u svakom segmentu se nalaze odgovarajući elementi.
// funkcija organizuje elemente vektora u tri dela:
// prvo elementi iz intervala (-Inf, A), zatim
// elementi iz intervala [A, B] i na kraju
// elementi iz intervala (B, Inf)
void podelaNiza(vector<int>& niz, int A, int B) {
// - na pozicijama [0, l) su elementi iz intervala (-Inf, A)
// - na pozicijama [l, i) su elementi iz intervala [A, B]
// - na pozicijama [i, d) su jos neispitani elementi
// - na pozicijama [d, n) su elementi iz intervala (B, Inf)
int l = 0, i = 0, d = niz.size();
// dok god postoje neispitani elementi
while (i < d) {
if (niz[i] < A)
// menjamo tekuci element sa prvim elementom iz [A, B]
swap (niz[i++], niz[l++]);
else if (niz[i] <= B)
// tekuci element ostaje na svom mestu
i++;
else
// menjamo tekuci element sa poslednjim neispitanim
swap(niz[i], niz[--d]);
}
}#include <iostream>
#include <vector>
#include <algorithm>
using namespace std;
// funkcija ucitava elemente u vektor
vector<int> unosNiza() {
int n;
cin >> n;
vector<int> a(n);
for (int i = 0; i < n; i++)
cin >> a[i];
return a;
}
// funkcija organizuje elemente vektora u tri dela:
// prvo elementi iz intervala (-Inf, A), zatim
// elementi iz intervala [A, B] i na kraju
// elementi iz intervala (B, Inf)
void podelaNiza(vector<int>& niz, int A, int B) {
// - na pozicijama [0, l) su elementi iz intervala (-Inf, A)
// - na pozicijama [l, i) su elementi iz intervala [A, B]
// - na pozicijama [i, d) su jos neispitani elementi
// - na pozicijama [d, n) su elementi iz intervala (B, Inf)
int l = 0, i = 0, d = niz.size();
// dok god postoje neispitani elementi
while (i < d) {
if (niz[i] < A)
// menjamo tekuci element sa prvim elementom iz [A, B]
swap (niz[i++], niz[l++]);
else if (niz[i] <= B)
// tekuci element ostaje na svom mestu
i++;
else
// menjamo tekuci element sa poslednjim neispitanim
swap(niz[i], niz[--d]);
}
}
// ispis elemenata vektora na standardni izlaz
void ispisNiza(const vector<int>& a, int A, int B) {
int i = 0;
// ispisujemo elemente iz intervala (-Inf, A)
while (i < a.size() && a[i] < A)
cout << a[i++] << " ";
cout << endl;
// ispisujemo elemente iz intervala [A, B]
while (i < a.size() && a[i] <= B)
cout << a[i++] << " ";
cout << endl;
// ispisujemo elemente iz intervala (B, +Inf)
while (i < a.size())
cout << a[i++] << " ";
cout << endl;
}
int main() {
// ucitavamo elemente niza
vector<int> a = unosNiza();
// ucitavamo interval [A, B]
int A, B;
cin >> A >> B;
// reorganizujemo elemente po intervalima (-inf, A), [A, B] i [B, inf)
podelaNiza(a, A, B);
// ispisujemo elemente niza
ispisNiza(a, A, B);
return 0;
}Primer 1.4.1. Razmotrimo rad algoritma na jednom primeru. Neka je \(A=4\), \(B=7\) i neka niz ima sadržaj 5 1 8 6 3 9 4 2. U nastavku ćemo prikazati stanje niza tokom izvođenja algoritma.
Nakon inicijalizacije promenljivih stanje je sledeće.
| l | d | |||||||
| 5 | 1 | 8 | 6 | 3 | 9 | 4 | 2 | |
| i |
Element \(5\) na poziciji \(i\) pripada intervalu \([A, B]\), pa se samo uvećava pokazivač \(i\).
| l | d | |||||||
| 5 | 1 | 8 | 6 | 3 | 9 | 4 | 2 | |
| i |
Element \(1\) na poziciji \(i\) pripada intervalu \((-\infty, A)\), pa se razmenjuje sa elementom \(5\) na poziciji \(l\) i oba pokazivača \(i\) i \(l\) se uvećavju.
| l | d | |||||||
| 1 | 5 | 8 | 6 | 3 | 9 | 4 | 2 | |
| i |
Element \(8\) na poziciji \(i\) pripada intervalu \((B, +\infty)\), pa se menja sa prvim elementom ispred pozicije \(d\) (što je element \(2\)) i pokazivač \(d\) se umanjuje.
| l | d | ||||||
| 1 | 5 | 2 | 6 | 3 | 9 | 4 | 8 |
| i |
Element \(2\) na poziciji \(i\) pripada intervalu \((-\infty, A)\), pa se razmenjuje sa elementom \(5\) na poziciji \(l\) i oba pokazivača \(i\) i \(l\) se uvećavju.
| l | d | ||||||
| 1 | 2 | 5 | 6 | 3 | 9 | 4 | 8 |
| i |
Element \(6\) na poziciji \(i\) pripada intervalu \([A, B]\), pa se samo uvećava pokazivač \(i\).
| l | d | ||||||
| 1 | 2 | 5 | 6 | 3 | 9 | 4 | 8 |
| i |
Element \(3\) na poziciji \(i\) pripada intervalu \((-\infty, A)\), pa se razmenjuje sa elementom \(5\) na poziciji \(l\) i oba pokazivača \(i\) i \(l\) se uvećavju.
| l | d | ||||||
| 1 | 2 | 3 | 6 | 5 | 9 | 4 | 8 |
| i |
Element \(9\) na poziciji \(i\) pripada intervalu \((B, +\infty)\), pa se menja sa prvim elementom ispred pozicije \(d\) (što je element \(4\)) i pokazivač \(d\) se umanjuje.
| l | d | ||||||
| 1 | 2 | 3 | 6 | 5 | 4 | 9 | 8 |
| i |
Element \(4\) na poziciji \(i\) pripada intervalu \([A, B]\), pa se samo uvećava pokazivač \(i\).
| l | d | ||||||
| 1 | 2 | 3 | 6 | 5 | 4 | 9 | 8 |
| i |
Pošto \(i\) dostiže vrednost \(d\), algoritam se završava. Elementi na pozicijama \([l, d)\) su iz intervala \([A, B]\), levo od njih su manji elementi, a desno veći.
U narednom apletu možete proveriti svoje razumevanje ovog algoritma.
✖
Uz terazije stoji skup tegova celobrojnih masa. Odrediti koja je najmanja celobrojna masa koja se ne može izmeriti pomoću tih tegova (svaki teg se može upotrebiti samo jednom).
Napomena: masa tela se uz pomoć terazija meri tako što se na jedan tas stavi to telo, a na drugi tegovi koje imamo na raspolaganju, tako da terazije budu u ravnoteži.
Sa standardnog ulaza se učitava broj \(n\) (\(1 \leq n \leq 10^3\)), a zatim u narednom redu sortiran niz od \(n\) prirodnih brojeva manjih od \(10^4\), koji predstavljaju skup masa tegova.
Na standardni izlaz ispisati traženi najmanji prirodan broj koji nije zbir nekih elemenata tog skupa.
8 1 2 4 7 15 32 35 48
30
Pomoću tegova mase \(m_0, \ldots, m_i\) sigurno ne možemo da izmerimo mase veće od \(Z_i = m_0 + \ldots + m_i\). Pitanje je da li možemo izmeriti sve mase iz intervala \([0, Z_i]\).
Činjenica da su elementi sortirani olakšava rešenje zadatka. Obrađivaćemo element po element i prilikom dodavanja svakog novog tega mase \(m_i\) proveravaćemo da li u intervalu \([0, Z_i]\) postoji neka masa koja se ne može izmeriti ili na snazi ostaje invarijanta da je moguće izmeriti sve mase iz \([0, Z_i]\).
Pretpostavimo da se tegovima \(m_0, \ldots, m_{i}\) mogla izmeriti svaka masa iz intervala \([0, Z_{i}]\). Tada se dodavanjem tega \(m_{i+1}\) može izmeriti svaka masa iz intervala \([0 + m_{i+1}, Z_{i} + m_{i+1}] = [m_{i+1}, Z_{i+1}]\) (dodavanjem tega \(m_{i+1}\) na prethodno odabrane tegove). Ako je novi učitani element \(m_{i+1} > Z_i + 1\), onda se \(Z_i + 1\) ne može izmeriti (jer je niz sortiran, pa su mase svih preostalih tegova veće ili jednake \(m_{i+1}\)), i to je tražena vrednost. U suprotnom, unija intervala \([0, Z_i] \cup [m_{i+1}, Z_{i+1}]\) pokriva interval \([0, Z_{i+1}]\), pa se sve mase iz tog intervala mogu izmeriti i invarijanta ostaje na snazi.
Primer 1.4.2. Na primer, neka je dat niz \(1, 2, 3, 5, 14, 20, 27\).
int n;
cin >> n;
// invarijanta: sabiranjem elemenata trenutnog obradjenog
// skupa tegova mogu se dobiti sve mase iz intervala [0, zbir]
int zbir = 0;
for (int i = 0; i < n; i++) {
int m; cin >> m;
if (m > zbir + 1)
break;
zbir += m;
}
cout << zbir + 1 << endl;#include <iostream>
using namespace std;
int main() {
int n;
cin >> n;
// invarijanta: sabiranjem elemenata trenutnog obradjenog
// skupa tegova mogu se dobiti sve mase iz intervala [0, zbir]
int zbir = 0;
for (int i = 0; i < n; i++) {
int m; cin >> m;
if (m > zbir + 1)
break;
zbir += m;
}
cout << zbir + 1 << endl;
return 0;
}Dokažimo korektnost ovog algoritma.
Lema 1.4.3. Neka je \(Z\) tekuća vrednost promenljive zbir. Invarijanta petlje je da je \(0 \leq i \leq n\), da je \(Z\) zbir prvih \(i\) elemenata niza i da se svaki broj iz intervala \([0, Z]\) može dobiti kao zbir nekog podskupa prvih \(i\) elemenata niza.
Dokaz. Pre ulaska u petlju je \(i=0\) i \(Z=0\). Zbir prvih \(i=0\) elemenata niza je po definiciji nula (tj. \(Z\)). Broj \(0\) je jedini element intervala \([0, Z] = [0, 0]\) i on se može dobiti kao zbir praznog podskupa (tj. 0 elemenata polaznog niza).
Obeležimo sa \(Z\) i \(i\) vrednosti promenljivih zbir i i pre ulaska u petlju, a sa \(Z'\) i \(i'\) vrednosti nakon izvršavanja tela i koraka petlje. Pretpostavimo da invarijanta važi pre ulaska u petlju.
Ako je \(m_i > Z+1\), tvrdimo da je \(Z+1\) traženi najmanji broj. Na osnovu invarijante znamo da su svi brojevi iz intervala \([0, Z]\) pokriveni, tako da manji broj od \(Z+1\) ne može biti rešenje. Dokažimo da broj \(Z+1\) ne može biti zbir nekog podskupa tegova. Pošto je niz sortiran, važi \(Z+1 < m_i \leq m_{i+1} \leq \ldots \leq m_{n-1}\). Dakle, ni jedan od tih elemenata ne sme biti uključen u podskup jer bi njihovim uključivanjem zbir već premašio \(Z+1\). Podskup se mora sastojati samo od elemenata \(m_0\) do \(m_{i-1}\), međutim, pošto je \(Z\) njihov zbir, zbir svakog njihovog podskupa je manji ili jednak \(Z\). Dakle, \(Z+1\) se ne može izmeriti i on je traženo rešenje.
Ako je \(m_i \leq Z+1\), tada je \(Z' = Z + m_i\), \(i' = i + 1\) i tvrdimo da je \(Z'\) zbir svih elemenata \(m_0\), …, \(m_i\) i da se svaki broj iz intervala \([0, Z']\) može predstaviti kao zbir nekog podskupa prvih \(i'\) elemenata niza. Prva tvrdnja je prilično očigledna, jer je po pretpostavci \(Z\) zbir svih elemenata \(m_0\), …, \(m_{i-1}\), a \(Z' = Z+m_i\). Na osnovu pretpostavke znamo da svi brojevi iz \([0, Z]\) mogu biti zbirovi podskupova prvih \(i\) elemenata niza. Slično i svi brojevi iz intervala \([m_i + 0, m_i + Z]\) se mogu dobiti kao zbir nekog podskupa prvih \(i' = i+1\) elementa niza. Naime, taj podskup će biti unija elementa \(m_i\) i onog podskupa prvih \(i\) elemenata niza čiji je zbir jednak razlici između tog broja i broja \(m_i\) — on je iz intervala \([0, Z]\), pa na osnovu pretpostavke takav podskup postoji. Pošto je \(m_i \leq Z + 1\) unija intervala \([0, Z]\) i \([m_i, m_i+Z]\) je \([0, m_i+Z] = [0, Z']\). Zato je svaki element iz \([0, Z']\) jednak zbiru nekog podskupa prvih \(i'\) elemenata niza, pa invarijanta ostaje očuvana. \(\Box\)
Teorema 1.4.6. Kada se program završi, vrednost \(Z+1\) je najmanji prirodni broj koji se ne može predstaviti kao zbir unetih brojeva.
Dokaz. Slučaj kada se petlja završi prekidom, jer je \(m_i > Z+1\) je već razmotren. Kada se petlja završi, važi da je \(i = n\). Na osnovu invarijante \(Z\) je zbir svih elemenata niza, i svaki broj iz \([0, Z]\) jeste zbir nekog podskupa prvih \(i=n\) elemenata niza, tj. celog niza. Zato je \(Z+1\) najmanji element koji nije moguće dobiti (jer se uključivanjem svih elemenata dobija najviše \(Z\)) i prikazano rešenje je ispravno. \(\Box\)
U narednom apletu možete videti kako ovaj algoritam funkcioniše.
✖
Ne postoji opšti postupak kojim se za proizvoljni zadati program može utvrditi da li se on zaustavlja za zadate vrednosti argumenata2. Ipak, za mnoge konkretne programe, može se utvrditi da li se zaustavljaju ili ne. Kako ne postoji opšti postupak koji bi se primenio na sve programe, zaustavljanje svakog programa mora se ispitivati zasebno i koristeći specifičnosti tog programa.
U programima u kojima su petlje jedine naredbe koje mogu dovesti do nezaustavljanja potrebno je dokazati zaustavljanje svake pojedinačne petlje. Ovo se obično radi tako što se definiše dobro zasnovana relacija3 takva da su susedna stanja kroz koje se prolazi tokom izvršavanja petlje međusobno u relaciji. Kod elementarnih algoritama ovo se obično radi tako što se izvrši neko preslikavanje skupa stanja u skup prirodnih brojeva i pokaže da se svako susedno stanje preslikava u manji prirodan broj.4 Pošto je relacija \(>\) na skupu prirodnih brojeva dobro zasnovana, i ovako definisana relacija na skupu stanja biće dobro zasnovana. Veličina koja se menja (smanjuje) tokom izvršavanja petlje naziva se varijanta petlje.
Razmotrimo nekoliko primera.
Iterativni algoritam koji vrši stepenovanje uzastopnim množenjem se zaustavlja. Zaista, u svakom koraku petlje vrednost \(n-i\) je prirodan broj (jer invarijanta kaže da je \(0 \leq i \leq n\)). Ova vrednost opada kroz svaki korak petlje (jer se \(n\) ne menja, a \(i\) raste), pa u jednom trenutku mora da dostigne vrednost \(0\).
Rekurzivna funkcija koja vrši brzo stepenovanje se zaustavlja. Zaista, u svakon narednom rekurzivnom pozivu vrednost \(n\) je strogo manja od trenutne. Zaista, rekurzivni pozivi se vrše samo kada je \(n > 0\). Ako je \(n\) parno, vrednost \(n/2\) je strogo manja od \(n\) (jer je tada \(n \geq 2\)), a ako je neparna, vrednost \(n-1\) je strogo manja od \(n\). Pošto je \(n\) prirodan broj on mora u nekom trenutku dostići vrednost \(0\), kada se izlazi iz rekurzije.
Nije poznato da li se naredna funkcija zaustavlja za proizvoljnu ulaznu vrednost \(n\).5
void f(unsigned n)
{
while (n > 1) {
if (n % 2)
n = 3*n+1;
else
n = n/2;
}
}Opšte uverenje je da se funkcija zaustavlja za svaku ulaznu vrednost \(n\) (to tvrdi još uvek nepotvrđena Kolacova (Collatz) hipoteza iz 1937). Navedeni primer pokazuje kako pitanje zaustavljanja čak i za neke veoma jednostavne programe može da bude ekstremno komplikovano.
Sva dosadašnja razmatranja o korektnosti programa vršena su zapravo poluformalno, tj. nije postojao precizno opisan formalni sistem u kojem se vrši dokazivanje korektnosti imperativnih programa. Jedan od najznačajnijih formalnih sistema ovog tipa opisao je Toni Hor (engl. Tony Hoare).
Semantika određenog programskog koda može se zapisati trojkom oblika
\[\{\varphi\} {\texttt P} \{\psi\}\]
gde je P niz naredbi, a \(\{\varphi\}\) i \(\{\psi\}\) su logičke formule koje opisuju veze između promenljivih koje se javljaju u tim naredbama. Trojku \((\varphi, {\texttt P}, \psi)\) nazivamo Horova trojka. Interpretacija trojke je sledeća: “Ako izvršenje niza naredbi P počinje sa vrednostima ulaznih promenljivih (u stanju) koje zadovoljavaju uslov \(\{ \varphi \}\) i ako P završi rad u konačnom broju koraka, tada vrednosti programskih promenljivih (stanje) zadovoljavaju uslov \(\{ \psi \}\)”. Uslov \(\{ \varphi \}\) naziva se preduslov, a uslov \(\{ \psi \}\) naziva se postuslov (posleuslov).
Na primer, trojka \(\{x=1\}\)y:=x\(\{y=1\}\)6, opisuje dejstvo naredbe dodele i kaže da, ako je vrednost promenljive \(x\) bila jednaka \(1\) pre izvršavanja naredbe dodele, i ako se naredba dodele izvrši, tada će vrednost promenljive \(y\) biti jednaka \(1\). Ova trojka je tačna. S druge strane, trojka \(\{x=1\}\)y:=x\(\{y=2\}\) govori da će nakon dodele vrednost promenljive \(y\) biti jednaka \(2\) i ona nije tačna. Specifikacija programa se može zadati u obliku Horove trojke. Na primer, specifikacija funkcije stepenovanja se može zadati u sledećem obliku:
\[\{n \geq 0 \wedge (n = 0 \Rightarrow x \neq 0)\}\texttt{s := stepen(x, n)}\{s = x^n\}\]
Horovom logikom se definišu pravila kojima se od jednostavnijih Horovih trojki izvode složenije. Opis ovih pravila i primer njihove primene na dokaz korektnosti funkcije stepenovanja dati su u poglavlju 1.A.3.
Formalni dokazi (u jasno preciziranom logičkom okviru) su važni 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 automatska provera neformalnog dokaza nije moguća). Softver čija je ispravnost dokazana i proverena automatski od strane namenskih programa je najpouzdaniji softver i zahtevi za takvim nivoom pouzdanosti postavljaju se za neke bezbednosno kritične aplikacije (kao što je, na primer, kontrolni softver za metro).
Kada se program i dokaz njegove korektnosti istovremeno razvijaju, programer bolje razume sam program i njegova svojstva. Metodologija formalnog ispitivanja ispravnosti utiče i na preciznost, konzistentnost i kompletnost specifikacije, na jasnoću implementacije i sklad implementacije i specifikacije. Zahvaljujući tome dobija se pouzdaniji softver, čak i onda kada se formalni dokaz ne izvede eksplicitno.
Ova teorema se može dokazati i principom jake indukcije za prirodne brojeve, u kom se iz induktivne pretpostavke da svi brojevi manji ili jednaki \(k\) imaju neko svojstvo dokazuje da i broj \(k+1\) ima to svojstvo. Međutim, princip indukcije koji prati definiciju rekurzivne funkcije je opštiji, jer se može primeniti i na funkcije čiji argumenti nisu prirodni brojevi ili jesu prirodni brojevi, ali se ne smanjuju monotono tokom rekurzivnih poziva. Stoga ćemo u svim dokazima koristiti ovaj opštiji princip, koji važi za sve rekurzivne funkcije koje se zaustavljaju za sve vrednosti svojih argumenata.↩︎
Ovo je čuveni halting-problem čiju je neodlučivost prvi dokazao Alan Tjuring.↩︎
Za relaciju \(\succ\) se kaže da je dobro zasnovana (engl. well founded) ako ne postoji beskonačan opadajući lanac elemenata \(a_1 \succ a_2 \succ \ldots\).↩︎
Smatramo da i nula pripada skupu prirodnih brojeva.↩︎
Pošto je opseg tipa unsigned ograničen, u ovom konkretnom primeru se mogu testirati sve moguće vrednosti za \(n\), međutim, u opštem slučaju, ako razmotrimo bilo koji mogući prirodan broj \(n\), tada je zaustavljanje nepoznato.↩︎
Prilikom opisa Horove logike, umesto C-ovske, biće korišćena sintaksa slična sintaksi korišćenoj u originalnom Horovom radu, gde se dodela umesto operatorom = označava operatorom :=.↩︎