> > Głównie dlatego, że testowanie jest zrozumiałe zarówno dla tych,
> > którzy to robią, jak i dla tych, którzy to mają zaakceptować jako
> > element projektu (czytaj: zapłacić za to lub uznać jego ważność). W
> > przeciwieństwie do dowodów, które są niezrozumiałe i stąd też
> > niechętnie akceptowane.
>
> No więc pomijając płacenie itd., to jest bardzo istotne kryterium, bo
> jeśli formalny zapis nawet nie tylko samego dowodu, ale również
> kryterium poprawności, które zostało dowiedzione, jest niezrozumiałe dla
> osób, które rozmieją, kiedy program jest rzeczywiście poprawny, to cały
> dowód poprawności jest OKDR.

Zgadza się. Ale z drugiej strony, skąd osoby, które rozumieją, kiedy program jest
rzeczywiście poprawny, mają pewność, że on faktycznie jest poprawny, skoro nie
potrafią wyspecyfikować tego kryterium? Kierują się przeczuciem?

Tak jak przeczuciem kierowali się ludzie, którzy dekadę temu napisali algorytm
sortowania w Javie?

http://envisage-project.eu/proving-android-java-and-
python-sorting-algorithm-is-broken-and-how-to-fix-it
/

Zgadzam się, że to jest problem. Metody formalne są ciałem obcym w branży, bo nie
pasują do dotychczas przyjętych wzorów pracy.

> > Zainteresowanie dowodzeniem rośnie właśnie dlatego, że jest
> > tańsze. Może być nawet dużo tańsze.
>
> Stąd gdzie ja stoję, tego zainteresowania nie widać.

Najwyraźniej nie ma takiej potrzeby.

> > Masz rację, że w finansach nie stosuje się dowodów ale nie dlatego,
> > że są droższe od testów, tylko dlatego, że testów też się tam nie
> > robi.
>
> Nie wątpię, że nieskończenie lepiej ode mnie znasz się na metodach
> formalnych, ale w tej kwestii nie masz pojęcia o czym mówisz.

Może tak być. Ale zadam dwa pytania kontrolne:

1. Czy ktoś poniósł kiedyś osobiste konsekwencje (np. poszedł do pierdla) za
zrobienie błędu w programie użytym w branży finansowej?
2. Czy ktoś odniósł kiedyś osobiste korzyści (np. dostał wysoką premię) za szybkie
wdrożenie systemu na rynek, wyprzedzając tym konkurencję?

Hę?

> 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).

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.

Ćwiczenie logiczne: jeżeli ktoś twierdzi, że testuje swój program, to ja poproszę o
*dowód*, że testowanie jest kompletne. Trudność w przeprowadzeniu takiego dowodu jest
dokładnie taka sama (i z tych samych powodów), jak dowód poprawności programu z
pominięciem testów, bo materiał wyjściowy jest dokładnie ten sam.

Różnica między dowodami i testami jest taka, że niekompletnego dowodu nie da się
zrobić, bo od razu widać, że jest niekompletny - natomiast bez najmniejszego problemu
można zrobić niekompletne testy, bo najczęściej nie widać, jak bardzo one są
niekompletne. Testy są po prostu wygodniejsze zarówno dla tych, którzy je robią, jak
i dla tych, którzy je akceptują i to tłumaczy ich "silną pozycję rynkową".

--
Maciej Sobczak * http://www.msobczak.com * http://www.inspirel.com