W dniu piątek, 27 marca 2015 15:12:10 UTC+1 użytkownik Maciej Sobczak napisał:

> > Nie wiem, dlaczego programów napisanych w C++
> > miałoby się nie dać uruchomić z zamiarem sprawdzenia, jak się zachowuje
> > w określonych okolicznościach.
>
> Da się. Ale nie da się stwierdzić, czy te sprawdzone okoliczności wyczerpują
możliwe stany i zachowania sprawdzanego programu, adekwatnie do wszystkich możliwich
sposobów przyszłego użycia.

Da się z łatwością stwierdzić, że zazwyczaj nie wyczerpują.

> Przykładowo, da się napisać test, który "sprawdza" funkcję sortującą i zapewne ktoś
taki test napisał w Javie dla funkcji napisanej dekadę temu. Dało się to napisać i
uruchomić.
>
> Ale rzeczona funkcja nadal była zje-banana, co raczej rzuca cień i rysę na taką
metodę.

Mnie się zdaje, że to w ogólności jest "cieńka" metoda. Tym bardziej,
że wielu ideologów pisania testów mówią, że "im więcej, tym lepiej"
i że "testy nie muszą być elegancko napisane" -- problem jest taki,
że testy również potrafią czynić pewne założenia, które nie są kluczowe
z perspektywy projektu, a których zmiana w projekcie sprawi, że słita
testowa stanie się bezużyteczna.

> > I przy okazji kilka ciekawostek, które ostatnio przebiegły twittera:
> >
> > "What if you could write a test for a problem and have your compiler
automatically return a correct implementation?":
>
> Fajne. Zwłaszcza jak ktoś napisze zły test. Będzie miał wtedy złą implementację
pasującą idealnie do tego złego testu.
>
> Spuszczamy to z wodą.

A co jeśli ktoś napisze zły test i złą implementację? Taki sam klops.
Jednak artykuł w gruncie rzeczy nie opisywał tego, o czym mówił
ten nagłówek, tylko po prostu pewną odmianę programowania
deklaratywnego opartą o microsoftowy system.

> Podobnie jak automaty, który generują testy z implementacji. To jest taka sama
ściema. Implementacja i test to są dwa *niezależne* artefakty, które się uzupełniają
właśnie dzięki temu, że są niezależne. Jak ktoś generuje jedno z drugiego, to równie
dobrze mógłby jednego w ogóle nie robić.
> Np. umówmy się, że wtedy nie robimy testów. To bardzo popularna metoda jest.

Tzn. generowanie testów z implementacji rzeczywiście brzmi idiotycznie.
Jednak w drugą stronę to nie całkiem zachodzi. Jeżeli mamy system, który
na podstawie testów potrafi wygenerować sensowną implementację, to szacun.

> > Na tym chyba polega istotowa różnica między dowodem a testowaniem,
> > że dowód wyczerpuje wszystkie możliwości, a testowanie nie.
> > "Kompletne testowanie" byłoby właśnie -- po prostu -- dowodem.
>
> Dokładnie. Stąd właśnie bierze się potencjalny zysk z użycia dowodów, które w
porównaniu do kompletnych testów mogą być tańsze. Bo to, że dowody mogą być droższe
od niekompletnych testów, to jest argument dla Dilberta.

Ja jednak będę trwał na stanowisku, że testy są z założenia niekompletne,
bo obejmują pewne przypadki jednostkowe. I testy jako takie mają pewną
wartość. Podobnie jak program QuickCheck.

I owszem, zgodzę się, że fajniej jest mieć dowody poprawności, kiedy
tylko się da (choć nie wiem, czy akurat w logice Hoare'a), ale jedno
nie wyklucza drugiego. Tak jak fajnie np. w podręczniku do matematyki
mieć nie tylko definicje, twierdzenia i dowody, ale również przykłady.