Pa zato sto je formalni dokaz jedan od retih nacina da znas da li program radi ili ne :). Znas vec pricu, testiranjem se moze dokazati jedino da program ne radi, a za dokaz da program radi u svim slucajevima moras probati sve slucajeve :).
E uzgred to je jedini nacin da racunarstvo pretvorimo u nauku, da ne bude samo skup recepata. Ovako je mnogo blize matematici i mnogo blize pravoj nauci. Ali to je nesto sto ne mozes da razumes ako ti je bitno samo da napises program. Kao sto u arapskoj mtematici je bitno jedino da se primeni recept, i resi jednacina, a kako se doslo do nje, nema veze. Razlika izmedju nadrilekarstva i farmacije je u toj nauci (jedni probaju dok ne uspeju u velikom broju slucajeva, a drugi proucave formalno nesto).
To je i bio jedan moj test sa mali c programima, da vidim koliko njih ce krenuti da pravi teoriju o tome, ali nije niko.
Sto se tice ispita, na usmenom ispitu iz "Teorije Racunarastva" na prvoj godini posdiplomskih studija iz Racunarstva na Matematickom fakultetu Unievrziteta u Beogradu sam imao sledeci od 4 pitanja: Objasniti postupak eliminacije rekurzije sa dokazom korektnosti, primeniti na primeru algoritma kule Hanoja.
Dakle da bi dobio 10, morao sam da pored ostalog napisem iterativne kule hanoja.
Inace ne mora nuzno da se eliminise stekom rekurzija, ali tako rekurziju realizuje skoro svaki C kopajler :).
Inace sto se tice nerekurzivnih kula hanoja, spomenuo bi algoritam Nebojse Vasiljevica koji je to uradio bez steka, jednom for petljom. Koristio je brojeve u promenljivom brojnom sistemu:
0 -> 0
1 -> 1
2 -> 10
3 -> 11
4 -> 20
5 -> 21
6 -> 100
7 -> 101
8 -> 110
9 -> 111
10 -> 120
11 -> 121
12 -> 200
13 -> 201
14 -> 210
15 -> 211
16 -> 220
17 -> 221
18 -> 300
19 -> 301
20 -> 310
21 -> 311
22 -> 320
23 -> 321
24 -> 1000
Eto malo igre za one koji vole razmisljanje.
CHUPCKO