W dniu piątek, 27 marca 2015 21:25:34 UTC+1 użytkownik Andrzej Jarzabek napisał:

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

To skąd wiedzą, że dobrze wyspecyfikowały? Mają przeczucie?

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

I napisać funkcję sort?

> No więc właśnie algorytm sortowania to taki wdzięczny temat dla metdo
> formalnych

Tak. Metody formalne rozwija się po to, żeby wdzięcznych tematów było coraz więcej.

> Niestety w praktyce zwykle miewa się do czynienia z
> bardziej skomplikowanymi przypadkami.

Zgadza się. I co, wtedy się łatwo testuje?

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

Ale testy też się nie nadają, tylko łatwiej to ukryć pod pozorem, że się je robi.

> Konsensus jest taki, że metody formalne albo w ogóle nie
> nadają się do zastosowania większości problemów, albo są nieopłacalne.

Czyj konsensus? Bo na razie ustaliliśmy, że punkty widzenia są różne.

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

No więc ja rozumiem, że zainteresowanie jest.

> Tyle że na razie udaje
> się to jedynie w specyficznych niszach.

Bo tylko w specyficznych niszach się próbuje to robić. W pozostałych niszach może
nawet nie być wystarczającej świadomości, że jest to możliwe.

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

Nie wiem. Nie wiem nawet, czy to jest dobre pytanie. Bo zamiast szukać jednej metody
do zastosowania w ogólnym przypadku, może trzeba szukać szczególnej metody do każdego
przypadku osobno. Ja wiem, że korporacje tego nie lubią, bo im to utrudnia
zarządzanie zasobami metodą "zatrudnijmy 20% programistów więcej".

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

Sam napisałeś, że to wszystko wynika z zarządzania ryzykiem. Powyżej masz input do
tego zarządzania. Outputem jest wybór metod pracy.

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

Zgadza się. Coś jak z pytaniem czy dziecko nauczyło się tabliczki mnożenia a ono
odpowiada, że nauczyło się tyle, żeby w opłacalnym stopniu zredukować ryzyko wpadki.
No to nauczyło się czy się nie nauczyło?

> jest oczywistą
> oczywistością, że jakiekolwiek testowanie jest lepsze od braku
> testowania w ogóle.

Tak. Jest też oczywistą oczywistością, że jakiekolwiek testowanie nie wypełnia
definicji terminu "system jest przetestowany". Proponuję wprowadzić termin
"podtestowany system".

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

Złe pytanie. Tego programu jeszcze nie ma, więc nie ma takiego przypadku. :-)
Przypadkiem może być problem do rozwiązania, np. "system tradingowy". Mam opisać jak
się to robi od początku? No więc bierze się białą tablicę i pisak, a potem... ;-)

Ja wiem, że to jest niemodne podejście. Teraz się od razu nap...la kod, zanim jeszcze
będzie wiadomo, co program ma robić.

> Ale niekompletne testy są też użyteczne, w sensie takim, że realnie
> redukują ryzyko

Jak realnie? Możesz to wyrazić w liczbach? Jakiś wykres, abo coś? Bo jeśli mam za to
zapłacić, to chcę znać ROI. Skoro te testy mają mieć efektywność probabilistyczną, to
być może bardziej opłaca się wykupienie polisy ubezpieczeniowej? To wcale nie jest
śmieszne pytanie.

> w przeciwieństwie do niekompletnego dowodu, który jest
> czystym marnotrawstwem.

Więc róbmy dowód kompletny.

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