W dniu piątek, 27 marca 2015 10:06:11 UTC+1 użytkownik Maciej Sobczak napisał:
>
> > No to teraz całkowicie bez szydery i na poważnie spytam, jakie są
> > praktyczne możliwości. Mam powiedzmy program w C++, kilkaset tysięcy
> > linii kodu, korzysta z boosta, wątków, libc, bazy danych, MOM-a itd. -
> > co można zrobić żeby udowodnuć jego poprawność i ile to będzie kosztowało?
>
> Nie da się. Dla równowagi zauważmy jednak, że przetestować
> tego też się nie da, zresztą dokładnie z tych samych powodów
> (uwaga logiczna: z tezy że się nie da konsekwentnie wynika
> też teza, że się tego nie robi; można co najwyżej udawać że
> się robi pomijając milcząco tą drobną niedogodność, że się
> nie da i tak właśnie działa większa część branży, patrz też niżej).

Tutaj akurat widzę pomylenie pojęć. Testowanie to uruchamianie
programu z założeniem sprawdzenia, jak się zachowuje w określonych
okolicznościach. 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.

> Na poważnie - nie stosuje się metod formalnych a posteriori
> w odniesieniu do kodu, który nie był pisany z myślą o takich
> metodach. Problem stopu, Goedel, i podobne teoretyczne przeszkody.
> Natomiast da się napisać (i to udowodnić) poprawny program,
> jeśli się go pisze z myślą o takich metodach.
> Co ciekawe, dotyczy to również testów i to z takich samych powodów.

To jest ciekawe pytanie: jakie znacie systemy stworzone z myślą
o dowodzeniu poprawności napisanych w nich programów?

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?":
http://blogs.teamb.com/craigstuntz/2014/07/07/38818/

Microsoft (chyba wczoraj) wypuścił źródła systemu Z3 używanego w w/w
artykule: github.com/Z3Prover/z3

Dowód sprzeczności w systemie Coq: https://github.com/clarus/falso

> Ćwiczenie logiczne: jeżeli ktoś twierdzi, że testuje swój program,
> to ja poproszę o *dowód*, że testowanie jest kompletne.

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.