On Dec 22, 10:28 am, Roman W <b...@g...pl> wrote:
> On Thursday, December 22, 2011 9:55:37 AM UTC, Andrzej Jarzabek wrote:
> > Natomiast w praktyce testy automatyczne potrafią wyłapać całkiem sporo
> > błędów - nawet takie, które działają przez kilka czy kilkanaście
> > minut, nie mówiąc już o tym, że po prostu możesz mieć wydzieloną
> > maszynę do soak testów, która mieli różne scenariusze 24/7 - to nie
> > jest taki gigantyczny koszt, a można to zrobić niezależnie od tego czy
> > i jak bardzo formalnie się dowodzi.
>
> Problem polega na tym, ze dowolny test robisz dla danych, ktore znasz.
> Natomiast jezeli masz logiczny dowod, ze implementacja jest poprawna i
> algorytm jest poprawny, to wiesz ze zadziala dla dowolnych danych
> akceptowanych przez algorytm.

O ile dowód jest również poprawny.

do góry

On Dec 22, 10:47 am, Edek <e...@g...com> wrote:
> On 12/22/2011 11:15 AM, Andrzej Jarzabek wrote:
> > On Dec 22, 8:47 am, Edek<e...@g...com>  wrote:
> >> On 12/22/2011 01:09 AM, Andrzej Jarzabek wrote:
>
> >>> No więc jeśli wiesz, że błędna implementacja wysypie się raz na 1e4, to
> >>> jeśli zrobiłeś test, który odpala się 1e6 razy, to masz znacznie lepszą
> >>> gwarancję poprawności, niż gdybyś tylko zrobił dowód (pół)formalny.
>
> >> Bzdura...
> > Bzdura, że bzdura.
> Heh, powiedz dlaczego...

Nie pofatygowałeś się, żeby to zrobić ze swojej strony, to ja tez nei
czuję się w obowiązku.

do góry

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

do góry

On 12/22/2011 12:28 PM, Edek wrote:
> a o to trudno, jeżeli
> się ni w ząb tego nie rozumie.

To nie było adresowane do nikogo, miałem na myśli wielu
takich, co zmieniają genialne algorytmy, bo tak im się wydaje
prościej. Moja kulpa...

Edek

do góry

On 12/22/2011 11:57 AM, Paweł Kierski wrote:
>> Problem polega na tym, ze dowolny test robisz dla danych, ktore znasz.
>> Natomiast jezeli masz logiczny dowod, ze implementacja jest poprawna i
>> algorytm jest poprawny, to wiesz ze zadziala dla dowolnych danych
>> akceptowanych przez algorytm.
>
> Nie zawsze. Losowane dane (losowy przegląd przestrzeni danych) może
> coś istotnego wykryć.
>
> Oczywiście dowód poprawności algorytmu jest lepszy. Do tego trzeba
> jeszcze dodać dowód poprawności implementacji. Co w sumie jest zazwyczaj
> drogie. Testy mają szansę złapać błąd zanim znajdziesz go w trakcie
> przeprowadzania dowodu. Co oczywiście nie znaczy, że "przetestowane"
> oznacza "poprawne". Oznacza tylko "większa szansa, że jest poprawne".
>
> Decyzja, co robić (dowód, testy na dużej ilości danych), jest już
> decyzją biznesową.

Prawdziwe. Wwymaga świadomości tego, jak zachowują się
różne rozwiązania i które jest najlepsze zależnie od tego, co chce
się osiąganąć.

Ja nie wiem, czy dowód musi być droższy. Jeżeli jest już zweryfikowany,
nie wymaga utrzymania, a testy wymagają utrzymania. Oczywiście,
jeżeli ktoś nie myknie na algorytmie refactoringu wedle uznania.

Edek

do góry

On Thursday, December 22, 2011 10:58:29 AM UTC, Andrzej Jarzabek wrote:

> > Problem polega na tym, ze dowolny test robisz dla danych, ktore znasz.
> > Natomiast jezeli masz logiczny dowod, ze implementacja jest poprawna i
> > algorytm jest poprawny, to wiesz ze zadziala dla dowolnych danych
> > akceptowanych przez algorytm.
>
> O ile dowód jest również poprawny.

Dlatego uwazam, ze trzeba robic i to, i to.

RW

do góry

On Thursday, December 22, 2011 11:43:53 AM UTC, Edek wrote:

> Ja nie wiem, czy dowód musi być droższy. Jeżeli jest już zweryfikowany,
> nie wymaga utrzymania, a testy wymagają utrzymania. Oczywiście,
> jeżeli ktoś nie myknie na algorytmie refactoringu wedle uznania.

Na to pomaga komentarz w kodzie:

// All changes to this code must be subjected to code review by the domain expert. Or
you're fired.

do góry

W dniu 2011-12-22 12:28, Edek pisze:
[...]
>>> 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.
[...]

Kwestia świadomości, czym jest test. Po zmianie algorytmu wiem, że
formalny dowód się już nie stosuje, ale zostaję z testem, który sprawdza
mi przynajmniej jakiś drobny fragment przestrzeni danych. Jeśli muszę
mieć dowód formalny, to go i tak go będę robił. A dzięki staremu
testowi już wiem, że nie zrobiłem grubego błędu w implementacji nowego
algorytmu (oraz że nowy algorytm w ogóle ma szansę być zastosowany).

--
Paweł Kierski
n...@p...net

do góry

On 12/22/2011 01:32 PM, Roman W wrote:
> On Thursday, December 22, 2011 11:43:53 AM UTC, Edek wrote:
>
>> Ja nie wiem, czy dowód musi być droższy. Jeżeli jest już zweryfikowany,
>> nie wymaga utrzymania, a testy wymagają utrzymania. Oczywiście,
>> jeżeli ktoś nie myknie na algorytmie refactoringu wedle uznania.
>
> Na to pomaga komentarz w kodzie:
>
> // All changes to this code must be subjected to code review by the domain expert.
Or you're fired.

:D

"Goes without sayin'"

Edek

do góry

On 12/22/2011 01:45 PM, Paweł Kierski wrote:
> W dniu 2011-12-22 12:28, Edek pisze:
> [...]
>>>> 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.
> [...]
>
> Kwestia świadomości, czym jest test. Po zmianie algorytmu wiem, że
> formalny dowód się już nie stosuje, ale zostaję z testem, który sprawdza
> mi przynajmniej jakiś drobny fragment przestrzeni danych. Jeśli muszę
> mieć dowód formalny, to go i tak go będę robił. A dzięki staremu
> testowi już wiem, że nie zrobiłem grubego błędu w implementacji nowego
> algorytmu (oraz że nowy algorytm w ogóle ma szansę być zastosowany).
>

Przesadziłem trochę z tym, że test to coś głęboko w Hudsonie, można
zmienić kod i nic nie wyskoczy na dashboard. Nie wiem, czy wszyscy tak
używają testów, ale ja lubię testy właśnie za szybki feedback.

Tu nie mam nic przeciwko testom jako takim gdzieś jako pomocnicze
narzędzie, bo workflow jest inny: zanim zmienię, przeczytam dowód
i zrozumiem jak to działa, a potem test się przyda podczas robienia
zmian, dokładnie tak jak mówisz.

W algorytmach wątkowych - nie mówię o kilku lockach w dużym
systemie, tylko np. kolejki o danych właściwościach, 30 linii
kodu i publikacja - testów się używa czasami, żeby znaleźć
przykład, kiedy algorytm nie działa. Ale nie znam przykładu,
gdzie to zastępuje dowód. Spotkałem się tylko z "hmm, no
tak, ten dowód, może by tu to zmienić w algorytmie - kurde,
faktycznie testy nie przechodzą po zmianie" i nie są to unit
testy, tylko modele. Modele nie są zapisane kodem źródłowym,
więc nie da się trywialnie zautomatyzować testów zmian kodu.

Bardziej ogólnie, przypuszczam, że są dziedziny, gdzie testy
dają "prawie pewność" w sensie matematycznym, co już może
wystarczyć.

Edek

do góry