On Thursday, December 22, 2011 12:09:57 AM UTC, 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.

A jak w produkcji algorytm wykonuje sie 24h na dobe co 10 milisekund, to takie dowody
poprawnosci mozna sobie, hmm, wsadzic w rurke.

RW