On 12/22/2011 10:19 AM, Stachu 'Dozzie' K. wrote:
> On 2011-12-22, Edek<e...@g...com> wrote:
>> On 12/22/2011 01:09 AM, Andrzej Jarzabek wrote:
>>> On 21/12/2011 19:37, Edek wrote:
>>>>
>>>> Z samego programowania dowody (pół)formalne stosuje
>>>> się przy algorytmach wątkowych. Żaden unit test nie pokaże
>>>> błędu wielowątkowego, co najwyżej wysypie się np. raz na 1e4.
>>>
>>> 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...
>
> 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]. Logika
jest po prostu logiką, nie logiką humanistyczną, nie logiką
miszczów Javy, nie kobiecą, jest weryfikowalna - daje zupełną
gwarancję. 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.

Testy robi się używając do tego specjalizowanych narzędzi,
nie unit testów, tam eksponuje się częstość występowania
błędów przez uwypuklenie sekwencji czasowych wobec
prawdziwego zastosowania w kodzie, co daje o kilka rzędów
wielkości większe prawdopodobieństwo pokazania błędu,
nie czeka się miesiąc tylko kilka sekund. To nie jest
unit test, testuje się poprzez model i tylko po to,
żeby mieć szybko wynik.

Edek

[1] ... ludzie zazwyczaj w ten sposób tłumaczą, dlaczego
nie ma formy dowodu matematycznego, dlaczego używają
swojej umownej notacji, itd., żeby uniknąć zbędnych pytań
i czepiania się rzeczy tak naprawdę nieistotnych.