DNS etc.

[Martin `MJ' Mares]

Zdravim!

> Ja jsem rikal, ze lze korektnost DNS implementace prokazat.

   ... ale uz jste se nezminil o tom, jak :-)

> K cemu smeruji je, ze LZE dokazat spravnost programu. Program 
> ma nejaky VSTUP a ma nejaky, na nem zavisejici VYSTUP. Toto 
> prirazeni je jednoznacne (s prihlednutim na pripadnou modifikaci 
> chovani obsluhou nebo generatorem nahodnych cisel) a nezavisle 
> na zadnych dalsich (explicitne neuvazenych) parametrech.

   Jenze co je toto prirazeni jineho nez nejaky algoritmus? Napriklad
specifikace DNS je v podstate jenom preformulovany program v nejakem
logickem programovacim jazyce. Jinymi slovy nedokazujete spravnost
programu, nybrz ekvivalenci nejakych dvou programu, jsa veden virou,
ze jeden z nich je spravne.

> "Inzenyrske" teorie o tom, ze teoreticke metody jsou naprd a v 
> praxi se uvidi, jsou roztomily folklor...

   Teoreticke metody jsou sikovna vec, ale clovek by mel vedet, jaky vyznam
maji jejich vysledky. Pokud konstruujete algoritmus resici nejakou exaktne
zadanou ulohu, pak je bez diskuse, ze je rozumne, ba dokonce v podstate nutne,
jej dokazat. Ale v pripade DNS serveru uz nemam pocit, ze by se o jakekoliv
specifikaci dalo rici, ze je zarucene ve 100%ni shode s tim, co lide povazuji
za spravne.

   Doplnovani jednoduchych pravidel typu "na kazdy packet je nutno odpovedet"
nevede k cili, protoze pak bude libovolny realny DNS server nekorektni, protoze
mu muze dojit misto v bufferech a pak je proste nucen packet zahodit.

				Have a nice fortnight
-- 
Martin `MJ' Mares   <mj na ucw.cz>   http://atrey.karlin.mff.cuni.cz/~mj/
Faculty of Math and Physics, Charles University, Prague, Czech Rep., Earth
"COBOL -- Completely Outdated, Badly Overused Language"