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.

> Jak wielu programistów robi, TDD: test, implementacja, przeszło
> - czyli już zrobione.

Nie wiem, ale inteligentni programiści z jakimkolwiek doświadczeniem,
lub choćby tacy, którzy czytali o tym książkę, wiedzą o
obszarach-pułapkach, jakimi są np. wątki, i w związku z tym wiedzą, że
trzeba zrobić coś więcej. A jak sami nie wiedzą co, to mogą spytać
bardziej doświadczonych kolegów, albo chociażby przeczytać o tym
książkę. Freeman i Pryce mają np. bardzo sensowny rozdział o testowaniu
programów wielowątkowych w TDD.