Jednou z v∞cφ, kterΘ dnes velmi trßpφ snad vÜechny producenty softwaru, je kvalita jejich produkt∙ - neboli otßzka, zda skuteΦn∞ d∞lajφ to, co d∞lat majφ. Softwarov² pr∙mysl se s tφmto problΘmem vyrovnßvß nejΦast∞ji cestou testovßnφ (r∙zn²ch alfa- a beta-verzφ), co₧ ovÜem ne v₧dy p°inßÜφ k²₧enΘ v²sledky - jak dokazujφ ΦetnΘ chyby, kterΘ se objevujφ i ve finßlnφch verzφch komerΦnφch produkt∙. Jak by se asi vÜem ulevilo, kdyby existovala n∞jakß mo₧nost formßlnφho ov∞°enφ sprßvnosti program∙, schopnß po
dat pßdn² a nezvratn² d∙kaz o tom, ₧e urΦit² program je v po°ßdku, neobsahuje ₧ßdnΘ chyby a skuteΦn∞ "d∞lß to, co d∞lat mß".
Je asi p°irozenΘ, ₧e stejnß otßzka napadla i lidi, kte°φ se poΦφtaΦi zab²vajφ po teoretickΘ strßnce. Ti ale bohu₧el zjistili, ₧e nic takovΘho neexistuje a v principu ani existovat nem∙₧e. Tedy ₧e nikdy nebude existovat prost°edek, kter² by o libovolnΘm programu dokßzal s urΦitostφ zjistit, zda je sprßvn² Φi nikoli. Jak ale k tomuto zßv∞ru doÜli?
Na pomoc si vzali jeden z mo₧n²ch abstraktnφch model∙ poΦφtaΦe, Turing∙v stroj, o kterΘm je znßmo, ₧e je "stejn∞ tak siln² jako kter²koli poΦφtaΦ" (viz minul² dφl tΘto rubriky). Na n∞m zaΦali nejprve hledat odpov∞d na pon∞kud jednoduÜÜφ otßzku: je mo₧nΘ v₧dy rozhodnout o tom, zda se kter²koli Turing∙v stroj zastavφ? Neboli, p°evedeno zp∞t do sv∞ta reßln²ch poΦφtaΦ∙: je mo₧nΘ rozhodnout o tom, zda v²poΦet kterΘhokoli programu skonΦφ v koneΦnΘm Φase, nebo nikoli?
Tento zajφmav² problΘm dostal i svΘ vlastnφ jmΘno: halting problem neboli problΘm zastavenφ (mφn∞no: zastavenφ Turingova stroje). Bohu₧el se vÜak ukßzalo, ₧e nemß °eÜenφ. P°esn∞ji ₧e nenφ algoritmicky rozhodnutelnΘ, zda se libovoln² Turing∙v stroj (alias poΦφtaΦ s libovoln²m programem) v koneΦnΘm Φase zastavφ, Φi nikoli.
Tomuto v²sledku je ovÜem t°eba sprßvn∞ rozum∞t. ╪φkß toti₧, ₧e nikdy nebude existovat algoritmus, kter² by problΘm zastavenφ Turingova stroje °eÜil pro libovoln² program (resp. pro libovoln² Turing∙v stroj). Tφm ovÜem nenφ vylouΦeno, aby takov²to algoritmus existoval pro urΦitou podmno₧inu vÜech mo₧n²ch program∙ (Turingov²ch stroj∙) - neexistuje pouze takov², kter² by byl jeden a fungoval spolehliv∞ pro jak²koli program.
Jestli₧e ale nebude nikdy z principu mo₧nΘ rozhodnout o tom, zda libovoln² program v∙bec n∞kdy dopoΦφtß a skonΦφ, pak zcela jist∞ nebude mo₧nΘ rozhodnout ani o tom, ₧e to, co vypoΦφtß bude sprßvnΘ. No a prßv∞ to je ona zßpornß odpov∞∩ vÜem, kte°φ volajφ po mo₧nosti formßlnφho dokazovßnφ sprßvnosti program∙. Znovu je ale t°eba tΘto odpov∞di sprßvn∞ rozum∞t: nikdy nebude existovat prost°edek, kter² by dokßzal rozhodnout o sprßvnosti libovolnΘho programu. To samoz°ejm∞ neznamenß, ₧e by nebylo mo₧nΘ formß
ln∞ dokßzat sprßvnost n∞kter²ch specißlnφch program∙ - dnes dokonce existuje celß v∞dnφ disciplφna, kterß se dokazovßnφm sprßvnosti (neboli tzv. verifikacφ) program∙ zab²vß. Zatφm jde ale spφÜe o akademickou zßle₧itost, kterß nemß v∞tÜφ vliv na tvrdou realitu softwarovΘho trhu.
Tento Φlßnek m∙₧e b²t voln∞ Üφ°en, pokud se tak d∞je pro studijnφ ·Φely, na nev²d∞leΦnΘm zßklad∞ a se zachovßnφm tohoto dov∞tku. Podrobnosti hledejte zde, resp. na adrese
http://archiv.czech.net/copyleft.htm