On 12/22/2011 11:46 AM, Stachu 'Dozzie' K. wrote:
>>> Nie do końca. Jeśli napisałeś test*oraz* przeprowadziłeś dowód
>>> >> (pół)formalny, to jesteś lepiej zabezpieczony. ale AJ pewnie chciał
>>> >> zastąpić dowód testem.
>>> >>
>> >
>> > Nie. Dowód jest "pół"-formalny tylko z powodu notacji [1].
> Nie zrozumiałeś. Nacisk jest na spójnik "oraz". Dowód i test razem
> wzięte zabezpieczają lepiej (a na pewno nie gorzej) niż sam dowód albo
> niż sam test.
>

Zrozumiałem. W naukach społecznych "oraz" stosuje się inaczej niż
w logice algorytmów.

Z tym "a na pewno nie gorzej" to się nawet zgodzę, piłkarzom
też nie szkodzi ucałowanie medalika przed meczem.

>> Test oczywiście można zrobić, ale mam pytanie:
>> > skąd niby ma być wiadomo, że błąd występuje raz na 1e4 i
>> > przy jakich założeniach? Dowód formalny jest adekwatny,
>> > a test nic nie wnosi.
> Jeśli test nie przechodzi, to sygnał, że trzeba się czemuś przyjrzeć.
> I to prawdopodobnie kodowi, który się zmieniał (więc raczej nie kodowi
> testu). Nie mówię że test zastępuje dowód. Test może dowodowi *pomóc*.

I o to właśnie chodzi. Pomoc owszem jest zawsze wskazana, o ile
pochodzi ze źródła, które coś wnosi. Test nic nie wnosi, bo zmieniając
taki algorytm - jakkolwiek - dowód możesz wywalić do kosza, czyli
zostaje się z testem, który nie zapewnia poprawności, a więc daje -
tu jest ta *istotna* część - złudne poczucie bezpieczeństwa i
pewności, że wszystko jest cacy, kiedy najczęściej nie jest. Ja może
nie popieram traktowania z góry w stylu A.L., ale są dziedziny,
gdzie wymagane jest coś więcej, niż szczery entuzjazm wobec Agile i
testów.

Paradoksalnie logika dowodów formalnych jest taka sama jak testów.
W tym sensie, że wystarczy pokazać jeden błędny przypadek, aby cały
dowód można było przeanalizować jeszcze raz, bo jest śmieciowy. Ale
żeby coś takiego zrobić trzeba mieć podstawę, a o to trudno, jeżeli
się ni w ząb tego nie rozumie.

Edek