On 27/03/2015 10:06, Maciej Sobczak wrote:
>>
>> 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?

Ale może właśnie potrafią wyspecyfikować, ale niekoniecznie w języku
formalnym.

Albo nawet, co jest też częste, nie potrafią co prawda wystarczająco
precyzyjnie wyspecyfikować, ale programista potrafi dojść do tego
poprzez zadawanie pytań, zrozumienie celu jaki ma realizować program i
posługiwanie się przykładami.

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

No więc właśnie algorytm sortowania to taki wdzięczny temat dla metdo
formalnych - formalne wyspecyfikowanie kryterium posortowanej sekwencji
nie stanowi problemu i nie wymaga żadnej wiedzy domenowej. Mało też
prawdopodobne, że to kryterium ulegnie zmianie w przewidywalnej
przyszłości. Niestety w praktyce zwykle miewa się do czynienia z
bardziej skomplikowanymi przypadkami.

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

Bo się nie nadają do realizacji tych zaań, które zazwyczaj się realizuje.

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

Zależy jak to rozumieć. Potrzeba niezawodności owszem, jest, ale nie za
wszelką cenę. Konsensus jest taki, że metody formalne albo w ogóle nie
nadają się do zastosowania większości problemów, albo są nieopłacalne.

Jeśli konsensus się myli, to byłoby bardzo duże zainteresowanie tym, jak
by to zrobić w praktyce tak, żeby się opłacało. Tyle że na razie udaje
się to jedynie w specyficznych niszach.

Jeśli uważasz, że dałoby się stosować te metody w ogólnym przypadku, to
np. ja byłbym bardzo zainteresowany - jak?

>> 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ę?

Ale właściwie co to ma do rzeczy? Firma nie ponosi straty jeśli
pracownik nie idzie do pierdla? Jak ktoś dostaje albo nie dostaje premii
to znaczy że są albo nie ma testów?

Zamiast odpowiadać na non sequitury, odniosę się do tego, o czym
pisałeś: owszem, firmy ponoszą straty finansowe i utratę reputacji na
wskutek błędnie działającego oprogramowania, owszem, jeśli firma straci
pieniądze przez takie błędy w swoim oprogramowaniu, np. wysyłając
niekorzystne dla siebie zlecenia na giełdę, to nie da się ich odzyskać
przez "reklamacje", owszem, oprogramowanie się testuje.


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

Da się, bo sukces testowania to nie jest 100% wyeliminowanie szansy
błędu, tylko redukcja ryzyka strat w takim stopniu, żeby opłacało się to
firmie.

O ile trudno jest zmierzyć dokładnie o ile ryzyko jest redukowane przez
testy i ile dokładnie opłaca się w te testy inwestoować, o tyle
(przynajmniej kiedy nie stosuje się metod formalnych) jest oczywistą
oczywistością, że jakiekolwiek testowanie jest lepsze od braku
testowania w ogóle.

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

Jak konkretnie by to wyglądało w przypadku takiego programu, jaki opisałem?

> 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ą".

Ale niekompletne testy są też użyteczne, w sensie takim, że realnie
redukują ryzyko - w przeciwieństwie do niekompletnego dowodu, który jest
czystym marnotrawstwem.