On 2011-12-22, Edek <e...@g...com> wrote:
> 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].

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.

> 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.

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*.

--
Secunia non olet.
Stanislaw Klekot