Naprosto nechapu o cem mel tenhle clanek byt, co chtel dokazat, a cim mi mel prispet. Pritom by stacilo jen par vet na zacatku ktere by to treba objasnili pro debily jako sem ja. :) Fakt nechapu vo co go, sem uplne mimo, a to uz sem 2 dny strizlivy...
v clanok vysvetluje ze vo vseobecnosti si programator nemoze byt isty ci napisal korektny (= necykliaci) program pretoze neexistuje algoritmus ktory by bol schopny toto rozhodnutie urobit.
u trivialnych programov (95% programatorskej praxe) dokaze clovek odhalit "pohladom" resp. metodou pokus omyl, ale u zlozitejsich ako napr schemu DES http://homel.vsb.cz/~ves064/Des_1024x768.html
clovek pohladom neodhali nic.
teda DES uvadzam preto lebo ma nedavno napadla idea si kdesi na nete najst popis DESu a ho aj implementovat ale ked som uvidel tu schemu tak ma velmi rychlo presla chut.
Jeden z dovodov bol aj ten ze na odsledovanie spravnosti medzi stavov by som musel tieto stavy pravdepodobne rucne pocitat :(
To není tak docela pravda: U většiny programů, které napíšu, vím, jak jsem na ten algoritmus přišel, a proto i dovedu sestrojit důkaz toho, že program je správně. Háček je ovšem v tom, že pokud program nevznikl takto, jeho korektnost se zjišťuje těžko a ve vší obecnosti to ani algoritmicky nelze.
(Docela hezký případ, který se mi už několikrát stal, je, že někoho napadne algoritmus řešící nějaký problém a když už ho má skoro naprogramovaný, uvědomí si, že k tomu algoritmu došel naprosto chybnou úvahou a není si najednou vůbec jistý, jestli ten algoritmus funguje ... a tak se snaží najít vstup, pro který fungovat nebude, a ono to nejde a nejde a nejde, až po několika hodinách se mu podaří dokázat, že to opravdu vždycky funguje, i když vůbec není na první pohled jasné, proč by mělo, a že to je daleko efektivnější řešení než nějaké evidentně korektní, které koho napadne na první pokus, když zrovna neudělá tu správnou chybu :-) ).
Ještě poznámka: Příznivci vývoje softwaru pomocí formálních specifikací (tj. nejdříve se sepíše formální specifikace problému v nějakém jazyce, pak se programuje a pak se dokazuje, že program opravdu řeší problém podle specifikace) nechť mi prominou, ale i když jsem u obvyklých jednoduchých problémů velkým příznivcem dokazování, u interaktivních systémů a podobných věcí si opravdu nemyslím, že by to byla ta správná cesta -- prostě proto, že u takových programů bývá chyba velmi často v tom, co si _myslíte_, že by program měl dělat, čili ve specifikaci ... a popsanou formální metodou zajistíte pouze to, že máte dokonale korektní implementaci nesmyslu :-)
