On Dec 22, 9:06 am, Roman W <b...@g...pl> wrote:
> On Thursday, December 22, 2011 12:09:57 AM UTC, Andrzej Jarzabek wrote:
>
> > > 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.
>
> A jak w produkcji algorytm wykonuje sie 24h na dobe co 10 milisekund,
> to takie dowody poprawnosci mozna sobie, hmm, wsadzic w rurke.

Nie bardzo rozumiem, chodzi o to, żeby nie przeprowadzać tego
formalnego czy półformalnego dowodu, bo można go sobie wsadzić w
rurkę? Czy żeby nie testować, bo skoro masz dowód, to testy są
niepotrzebne?

Tzn. ja bym faktycznie ostrożnie się zgodził z twierdzeniem, że w
wielu przypadkach formalne lub półformalne dowody poprawności
programów wielowątkowych mają niską wartość - jeśli synchronizacja
wątków jest na tyle skomplikowana, że taki dowód będzie nietrywialny,
to prawdopodobnie należy ją uprościć, a nie przeprowadzać dowód.
Natomiast nawet jeśli zaprojektujes algorytm i przedstawisz jego
poprawność, to znacznie trudniej będzie ci udowodnić, że program
zadany twoim kodem źródłowym faktycznie realizuje ten algorytm, a nie
- na wskutek pomyłki - trochę inny.

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.