On 28/03/2015 18:22, Maciej Sobczak wrote:
>
>>> To skąd wiedzą, że dobrze wyspecyfikowały? Mają przeczucie?
>>
>> Stąd, że się na tym znają.
>
> Ale znają się na tym, co sami z tego rozumieją. A specyfikacja jest
> po to, żeby to ich rozumienie przekazać innym (np. programistom). I
> teraz jest problem: skąd taka osoba wie, że dobrze coś
> wyspecyfikowała, skoro jej rozumienie tematu jest niejawnie
> uzupełnione posiadaną wiedzą, której nie wyspecyfikowała, ale tego
> nie zauważyła? To jest powszechne zjawisko.

Zazwyczaj tak, że specyfikuje się w języku naturalnym i różnych innych
nieformalnych notacjach i klaruje się to np. na przykładach, przez
rozmowy, odpowiedzi na pytania, przekazanie szerszego kontekstu - nie
tylko "jak to ma działać" ale i "czemu to ma służyć" i "dlaczego powinno
działać właśnie tak".

>> W praktyce funkcję sort pisze się bardzo rzadko.
>
> W praktyce każdą rzecz pisze się jeszcze rzadziej. Tym bardziej nie
> ma pewności, czy wszyscy wszystko tak samo dobrze rozumieją.

Jest pewność w sensie wystarczająco dużego prawdopodobieństwa.

>> Wtedy da się w praktyce testować - przez co rozumiem osiągnięcie
>> akceptowalnej niezawodności przy akceptowalnych kosztach.
>
> Czyli biznes typu "wicie rozumicie". Jedna wielka szara strefa.

Nie rozumiem o co ci chodzi. Każdy biznes wiąże się z ryzykiem i
praktycznie często tak jest, że jakby się chciało wyeliminować wszelkie
ryzyko (choćby przez ubezpieczanie się od wszystkiego), to koszty tej
eliminacji przewyższą przychody z biznesu.

> Na budowie desek ma być tyle, żeby się nie zawaliło. Czy może być jedna
> mniej, niż ostatnio? Nie wiemy, bo w praktyce niczego nie mierzymy i
> nie wiemy, gdzie jesteśmy z parametrami.

Przecież mierzymy - to właśnie testy są pomiarami.

>> Ale jak najbardziej się nadają, bo testowane programy działają
>> wystarczająco często i per saldo zarabiają.
>
> Tak. Ale skoro już zarabiają, to nie poprzestajmy na tym, tylko
> optymalizujmy. Może mogłyby zarabiać więcej? Problem w tym, że bez
> dokładnej wiedzy o tym co uzyskaliśmy, nie wiadomo, co i jak
> zmienić.

Akurat takie rzeczy się mierzy.

Ale też, żeby np. mieć sposób na zarabianie więcej, czasem musisz
skorzystać z wiedzy kogoś, kto wie, co trzeba zrobić, żeby zarabiać
więcej, ale nie wyrazi ci tego językiem formalnym.

>> Noo chyba że masz matematyczny dowód na to, że metody formalne są
>> opłacalne?
>
> To oczywiście będzie zależało od wielu parametrów, w szczególności od
> tego, jaki jest koszt fakapu. Zwykle jest bardzo mały, więc jedyna
> rzecz, która jest faktycznie opłacalna, to klepanie kodu.

Nie wiem, co rozumiesz przez "bardzo mały". Fakapy na kilka miionów
dolarów nie są niczym niezwykłym, znany jest przypadek Knight Capital,
gdzie błąd techniczny spowodował wysłanie błednych zleceń na giełdę i
stratę około 400 milionów dolarów jeśli dobrze pamiętam.

>> Instytucje finansowe zajmują się zarabianiem pieniędzy
>
> Wszyscy sie tym zajmują. Nie napinajmy się, że instytucje finansowe
> niby mają jedną nóżkę bardziej.

Nic takiego nie mówię, jedynie, że w tym kontekście piszę o realności
strat. Jeśli błędne wysłanie zleceń na giełdę spowoduje np. 2 miliony
dolarów strat, to jest to dwa milony mniej na bilansie firmy i strata
jest jak najbardziej realna. Podobnie, jeśli firma dostanie karę od
regulatora.

>> A straty z błędów są jak najbardziej realne,
>
> Nie będę wybiegał poza tematykę grupy zagłębiając się w tą część
> wątku, bo na pewno bym wybiegł za daleko.

Może jednak? Na dzień dobry, może wyjaśnisz, jeśli firma przez błąd w
swoim oprogramowaniu wyśle na giełdę zleceniaa i straci na tym kasę, to
do kogo może zgłosić reklamację żeby odzyskać te pieniądze?

>> Program jest, coś robi, został napisany w warunkach jakiejś
>> potrzeby i był modyfikowane w warunkach zmieniających się potrzeb.
>> Moje pytanie jaką byś zaproponował metodę działania zamiast tej,
>> która faktycznie została zastosowana i doprowacziła do powstania
>> programu takiego, jaki jest.
>
> W systemie finansowym? Zrobiłbym go dokładnie takimi metodami, jakie
> opisałeś. Byłoby to w zgodzie z:
>
> 1. potencjalnymi kosekwencjami dla mnie w przypadku fakapu 2.
> potencjalnymi korzyściami, np. w postaci wysokich premii 3. mojej
> osobistej opinii nt. realności strat w tym systemie
>
> Serio. Ja też umiem liczyć.

No to policz taki wariant:

Jeśli zrobisz tak, jak opisałem, to dostaniesz normalną pensję, której
co nikt nie zabierze. Jeśli program zarobi pieniądze, dostaniesz jakąś
premię, ale bez szału. Jeśli bugi spowodują, że program straci dużo
kasy, nie dostaniesz premii, a może nawet wylecisz z pracy.

Jeśli wprowadzisz użyjesz metod formalnych i się nie powiedzie, to
również dostaniesz pensję i być może stracisz pracę. Jeśli się powiedzie
wyjątkowo dobrze (gdzie normą jest nie stosowanie metod formalnych), i
co więcej, będziesz potrafił wykazać, że w wielu wypadkach

> A teraz porozmawiajmy o pociągach. Albo windach. Albo sprzęcie
> medycznym. Albo o samochodach, to teraz dosyć popularny temat. Albo o
> czymkolwiek innym, gdzie, jak to mówi przysłowie, programista wiesza
> się razem ze swoim programem, zwłaszcza gdy sam staje się jego
> użytkownikiem.

No i co? Jak sprzęt medyczny czy samochód kogoś zabije, to programista,
etatowy pracownik producenta idzie siedzieć? Koleś od Therac-25 chyba
nie był nawet oskarżony?

>>> Skoro te testy mają mieć efektywność probabilistyczną, to być
>>> może bardziej opłaca się wykupienie polisy ubezpieczeniowej? To
>>> wcale nie jest śmieszne pytanie.
>>
>> Myślę, że nikt ci nie sprzeda takiej polisy.
>
> A ja myślę, że takie polisy będą. Razem z całym systemem wyliczania
> ich wysokości.

OIMW na razie nie ma niczego takiego. Więc nie ma takiej opcji.

Nie wyobrażam sobie zresztą, jak firma ubezpieczniowa miałaby szacować
ryzyko dla takiego programu - z wyjątkiem założenia, że wszystko się
spieprzy w najgorszy możliwy sposób?

>> To jest ryzyko, bo może się okazać, że zanim skończysz dowodzić,
>> skończą się pieniądze albo program przestanie być potrzebny w
>> takiej postaci.
>
> Widziałem też przypadek, kiedy skończyły się pieniądze na testy.

No właśnie o to chodzi, że jeśli po zrobieniu np. 75% testów, które się
zakładało zrobić, skończą się pieniądze, to te 75% testów nadal coś daje.

do góry

> > Czyli biznes typu "wicie rozumicie". Jedna wielka szara strefa.
>
> Nie rozumiem o co ci chodzi.

O świadomość. Tzn. o świadomość ograniczeń metod, którymi się posługujemy.
Ta świadomość zanika np. wtedy, gdy optymistycznie uznajemy, że coś przetestowaliśmy,
chociaż w rzeczywistości nie mamy nawet miary, która by ustaliła, w jakim stopniu to
zrobiliśmy i ostatecznie wiemy tylko jaki wysiłek w to włożylismy (np. ile godzin
poszło na testy) a nie ile przez to uzyskaliśmy.
Szukam metody, która byłaby bardziej obiektywna, niż "akceptowalność przez
konsensus".

> Przecież mierzymy - to właśnie testy są pomiarami.

Nie, chodzi mi o pomiar skuteczności testów. Tak naprawdę nie wiemy, w jakim stopniu
są skuteczne a przez to nie wiemy, kiedy przestać.

Spróbujmy tak: chcę, żeby system miał co najwyżej 1 buga na 10k linii kodu. Ile
dolarów mam wydać na pisanie testów? Ciemność.

To jest inny poziom myślenia, niż "akceptowalna jakość za akceptowalną cenę".

> No to policz taki wariant:
>
> Jeśli zrobisz tak, jak opisałem, to dostaniesz normalną pensję, której
> co nikt nie zabierze. Jeśli program zarobi pieniądze, dostaniesz jakąś
> premię, ale bez szału. Jeśli bugi spowodują, że program straci dużo
> kasy, nie dostaniesz premii, a może nawet wylecisz z pracy.

Podoba mi się słowo "może". Ale zgadza się.

> Jeśli wprowadzisz użyjesz metod formalnych i się nie powiedzie,

Co się nie powiedzie? Że program będzie poprawny ale jednak nie będzie?

> No i co? Jak sprzęt medyczny czy samochód kogoś zabije, to programista,
> etatowy pracownik producenta idzie siedzieć?

Dobre pytanie. Problem z odpowiedzią jest taki, że w tych branżach takich wypadków
jest zdumiewajaco mało, więc trudno mówić o powszechnie panujących regułach
postępowania. Sam napisałeś, że fakapy na kilka milionów w systemach finansowych nie
są niczym niezwykłym - rozumiem, że jest ich na tyle dużo, że istnieje jakiś
konsensus nt. tego, co należy wtedy zrobić. No i wychodzi na to, że niewiele się robi
("może nawet wylecisz z pracy" - z akcentem na "może"). Natomiast w branżach
krytycznych fakapów jest bardzo mało. Było kilka spektakularnych, ale powiedzmy, że
potrafimy znaleźć jeden przykład medyczny, jeden rakietowy, jeden yyy no nie wiem
jaki i właśnie z małej liczby takich przykładów wynika brak konsensusu, co dalej.
A teraz pytanie, z czego wynika mała liczba fakapów w takich branżach.

> Nie wyobrażam sobie zresztą, jak firma ubezpieczniowa miałaby szacować
> ryzyko dla takiego programu

No patrz, a w branżach krytycznych szacują.

I właśnie o tym piszę.

> > Widziałem też przypadek, kiedy skończyły się pieniądze na testy.
>
> No właśnie o to chodzi, że jeśli po zrobieniu np. 75% testów, które się
> zakładało zrobić, skończą się pieniądze, to te 75% testów nadal coś daje.

Ile daje? Tego właśnie nie wiemy. A czy lepiej by było zrobić wtedy inne testy, tzn.
inne 75%? Też nie wiemy. I nawet nie wiemy, co byśmy zyskali, gdybyśmy zrobili 100%
*założonych*. Intuicyjnie dałoby nam "coś" więcej, ale to jest taka sama intuicja,
jak to, że jak dam żebrakowi więcej, to spotka mnie większe szczęście.
Wiemy, ile nas to kosztowało ale nie wiemy, ile zyskaliśmy. Bo nie mamy jak zmierzyć.
I to jest ta szara strefa, która nie bardzo pasuje do inżynierskiego charakteru
naszej profesji. O tym właśnie piszę.

--
Maciej Sobczak

do góry

On 29/03/2015 00:13, Maciej Sobczak wrote:
>
>> Przecież mierzymy - to właśnie testy są pomiarami.
>
> Nie, chodzi mi o pomiar skuteczności testów. Tak naprawdę nie wiemy,
> w jakim stopniu są skuteczne a przez to nie wiemy, kiedy przestać.

W indywidualnym przypadkui nie wiemy, ale w skali dużej firmy jak
najbardziej można zbierać dane między wysiłkiem włożonym w testowanie s
stratami z fakapów.

Z tym że mnie np. nie przekonuje to, czy wiedza z takich danych jest
loepsza niż intuicja doświadczonego inżyniera oprogramowania.

> Spróbujmy tak: chcę, żeby system miał co najwyżej 1 buga na 10k linii
> kodu. Ile dolarów mam wydać na pisanie testów? Ciemność.
>
> To jest inny poziom myślenia, niż "akceptowalna jakość za
> akceptowalną cenę".

To jest bezużyteczny poziom myślenia, sensowne kryterium to np. jakie
jest prawdopodobieństwo, że program w ciągu roku straci więcej niż 3
miliony, więcej niż 2 miliony, że w ogóle straci, że zyska więcej niż
milion, więcej niż dwa miliony itd. - i w ten rachunek wlicza się straty
spowodowane przez bugi. I takie rzeczy się jak najbardziej szacuje.

>> dostaniesz jakąś premię, ale bez szału. Jeśli bugi spowodują, że
>> program straci dużo kasy, nie dostaniesz premii, a może nawet
>> wylecisz z pracy.
>
> Podoba mi się słowo "może". Ale zgadza się.

Na ile rozumiem, to jest dokładnie tak samo, jak w "branżach
krytycznych" - jeśli bug w oprogramowaniu kogoś zabije, to programista
na etacie może straci pracę a może nie, ale procesu karnego ani
cywilnego raczej nie musi się obawiać.

>> Jeśli wprowadzisz użyjesz metod formalnych i się nie powiedzie,
>
> Co się nie powiedzie? Że program będzie poprawny ale jednak nie
> będzie?

Oczywiście, że formalna zgodność programu z kryteriami zapisanymi w
języku formalnym nie oznacza, że program będzie rzeczywiście dobrze
realizował cel, do którego został stworzony.

Ale mnie ogólnie chodzi o to, że nawet w przypadku redukcji ryzyka
fakapu korzyść z tego będzie mniejsza niż całkowity koszt zastosowania
metod formalnych.

>> No i co? Jak sprzęt medyczny czy samochód kogoś zabije, to
>> programista, etatowy pracownik producenta idzie siedzieć?
>
> Dobre pytanie. Problem z odpowiedzią jest taki, że w tych branżach
> takich wypadków jest zdumiewajaco mało, więc trudno mówić o
> powszechnie panujących regułach postępowania.

Jest wystarczająco dużo żeby wiedzieć, czy to się w ogóle zdarza. Na ile
rozumiem, w wielu rozwiniętych krajach konstrukcja prawa jest taka, że
praktycznie jest to niemożliwe.

> Sam napisałeś, że
> fakapy na kilka milionów w systemach finansowych nie są niczym
> niezwykłym - rozumiem, że jest ich na tyle dużo, że istnieje jakiś
> konsensus nt. tego, co należy wtedy zrobić.

Nic mi o takim konsensusie nie wiadomo (z wyjątkiem ogólnego "zbadać
przyczyny i zastanowić się czy i jak można temu zapobiegać w przyszłości")

> No i wychodzi na to, że
> niewiele się robi ("może nawet wylecisz z pracy" - z akcentem na
> "może"). Natomiast w branżach krytycznych fakapów jest bardzo mało.
> Było kilka spektakularnych, ale powiedzmy, że potrafimy znaleźć jeden
> przykład medyczny, jeden rakietowy, jeden yyy no nie wiem jaki i

Pamiętam, że nie tak dawno temu była afera z hamulcami w samochodach.

> właśnie z małej liczby takich przykładów wynika brak konsensusu, co
> dalej.

I - niech zgadnę - wychodzi na to, że niewiele się robi - jeśli chodzi o
osobiste konsekwencje dla programisty - może nawet stracić pracę?

> A teraz pytanie, z czego wynika mała liczba fakapów w takich
> branżach.

Z różnych rzeczy może wynikać, choćby z tego, że system sterowania
hamulcem w samochodzie zapewne jest ileś tam rzędów wielkości mniej
skomplikowany od systemu do odtwarzania muzyki czy nawigacji
satelitarnej w tym samym samochodzie. Albo np. że nie jest tak, że
drogowcy co dwa miesiące wymieniają nawierzchnię na taką, na której
stare oprogramowanie źle działa. Albo że program do startu rakiety który
jest dobry dzisiaj, za dwa tygodnie będzie do wyrzucenia z powodu
niemożliwych do przewidzenia zmian w składzie atmosfery, właściwościach
chemicznych ciekłego tlenu i stałej grawitacyjnej.

>> Nie wyobrażam sobie zresztą, jak firma ubezpieczniowa miałaby
>> szacować ryzyko dla takiego programu
>
> No patrz, a w branżach krytycznych szacują.
>
> I właśnie o tym piszę.

Firmy ubezpieczeniowe?

>> No właśnie o to chodzi, że jeśli po zrobieniu np. 75% testów, które
>> się zakładało zrobić, skończą się pieniądze, to te 75% testów nadal
>> coś daje.
>
> Ile daje? Tego właśnie nie wiemy.

Nie wiemy w sensie że ja nie wiem i ty nie wiesz, to nie znaczy, że w
ogóle nie wiadomo.

> A czy lepiej by było zrobić wtedy inne testy, tzn. inne 75%?
> Też nie wiemy. I nawet nie wiemy, co byśmy
> zyskali, gdybyśmy zrobili 100% *założonych*. Intuicyjnie dałoby nam
> "coś" więcej, ale to jest taka sama intuicja, jak to, że jak dam
> żebrakowi więcej, to spotka mnie większe szczęście. Wiemy, ile nas to
> kosztowało ale nie wiemy, ile zyskaliśmy. Bo nie mamy jak zmierzyć. I
> to jest ta szara strefa, która nie bardzo pasuje do inżynierskiego
> charakteru naszej profesji. O tym właśnie piszę.

No nie wiem, mówisz, że w inżynierii lądowej wiedzą dokładnie o ile
wzrośnie prawdopodobieństwo zawalenia mostu jeśli będą prowadzić 15%
mniej dokumentacji albo stosować 10% mniej norm?

do góry

> W indywidualnym przypadkui nie wiemy, ale w skali dużej firmy jak
> najbardziej można zbierać dane między wysiłkiem włożonym w testowanie s
> stratami z fakapów.

I właśnie piszę o tym, że z tych zebranych danych rodzi się zainteresowanie metodami
formalnymi.

> Z tym że mnie np. nie przekonuje to, czy wiedza z takich danych jest
> loepsza niż intuicja doświadczonego inżyniera oprogramowania.

Intuicja doświadczonego programity nie zostaje w firmie gdy on odchodzi. Wiedza z
zebranych danych i wynikające z niej decyzje jak najbardziej mogą zostać i to też
przyczynia się do zainteresowania metodami, które są przewidywalne.

> > Podoba mi się słowo "może". Ale zgadza się.
>
> Na ile rozumiem, to jest dokładnie tak samo, jak w "branżach
> krytycznych" - jeśli bug w oprogramowaniu kogoś zabije, to programista
> na etacie może straci pracę a może nie, ale procesu karnego ani
> cywilnego raczej nie musi się obawiać.

Przecież nie napisałem, że zawsze chodzi o programistów. Najczęściej to nawet nie oni
wybierają metody pracy (jest odwrotnie: zwykle programiści są wybierani pod kątem
metody, która ma być zastosowana).
W branżach krytycznych jest jeszcze temat norm, które ten temat porządkują.

> Ale mnie ogólnie chodzi o to, że nawet w przypadku redukcji ryzyka
> fakapu korzyść z tego będzie mniejsza niż całkowity koszt zastosowania
> metod formalnych.

Jeśli korzyść z redukcji ryzyka fakapu będzie mniejsza od czegoś, czego nawet nie
wyceniłeś, to przyznajesz, że koszty fakapu są relatywnie niewielkie albo jego
prawdopodobieństwo epsilonowe - ale przyznałeś też, że milionowe fakapy nie są niczym
niezwykłym. Wychodzi mi to, co napisałem wcześniej - że fakapy są relatywnie tanie.

> Pamiętam, że nie tak dawno temu była afera z hamulcami w samochodach.

Tak - wyleciało mi to z głowy, a to bardzo dobry przykład do tej dyskusji.

Przykład jest dobry, bo pokazuje pewne mechanizmy, które w pewnych branżach występują
a w innych nie występują.
Mówimy o skandalu z Toyotą - zginęli ludzie. W przeciwieństwie do Twojego przykładu z
Knight Capital, gdzie regulatorzy uznali, że nie ma po co interweniować, z Toyotą
uznali, że jak najbardziej należy interweniować. Wtedy pojawił się audytor (1), który
wskazał na rażące niezgodności z obowiązującymi normami (2), co zakończyło się
wyrokiem w sądzie (3), a przy okazji działaniami korygującymi (4).

Ważne słowa: audyt, normy, sąd, działania korygujące.

Czy te słowa występują w branży finansowej? Mówimy o warstwie technicznej.

Działania korygujące wyglądają tak:

http://www.automotive-eetimes.com/en/toyota-utilizes
-spark-pro-programming-language-in-ultra-low-defect-
software.html?cmp_id=7&news_id=222902902

Panowie zauważyli, że:

"[...] it enables lower development and maintenance efforts since the formal approach
[...]"

I ja właśnie dokładnie o tym - o rosnącym zainteresowaniu metodami formalnymi, które
coraz częściej są postrzegane jako tańsza alternatywa dla testów.
Przy okazji wspomniałem też o tym, że branża finansowa nie jest poziomem
referencyjnym w temacie dbania o jakość produktów, chociaż wcale nie chciałem, aby
stało się to głównym tematem tego wątku.

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

do góry

On 29/03/2015 23:18, Maciej Sobczak wrote:
>
>> W indywidualnym przypadkui nie wiemy, ale w skali dużej firmy jak
>> najbardziej można zbierać dane między wysiłkiem włożonym w
>> testowanie s stratami z fakapów.
>
> I właśnie piszę o tym, że z tych zebranych danych rodzi się
> zainteresowanie metodami formalnymi.

No więc OIMW w finansach takie dane są zbierane, a zainteresowanie
metodami formalnymi z tego nie wynika.

>> Z tym że mnie np. nie przekonuje to, czy wiedza z takich danych
>> jest loepsza niż intuicja doświadczonego inżyniera oprogramowania.
>
> Intuicja doświadczonego programity nie zostaje w firmie gdy on
> odchodzi. Wiedza z zebranych danych i wynikające z niej decyzje jak
> najbardziej mogą zostać i to też przyczynia się do zainteresowania
> metodami, które są przewidywalne.

Można też zatrudnić kolejną osobę z doświadczeniem i to wg. mnie nadal
jest bardziej opłacalne niż metody formalne (z wyjątkiem nisz etc. etc.)

>> Na ile rozumiem, to jest dokładnie tak samo, jak w "branżach
>> krytycznych" - jeśli bug w oprogramowaniu kogoś zabije, to
>> programista na etacie może straci pracę a może nie, ale procesu
>> karnego ani cywilnego raczej nie musi się obawiać.
>
> Przecież nie napisałem, że zawsze chodzi o programistów. Najczęściej
> to nawet nie oni wybierają metody pracy (jest odwrotnie: zwykle
> programiści są wybierani pod kątem metody, która ma być
> zastosowana). W branżach krytycznych jest jeszcze temat norm, które
> ten temat porządkują.

Aha, a osobom wybierającym metody pracy realnie grozi powództwo karne
lub cywilne (w sensie że się coś takiego zdarzyło)? W przypadku, kiedy
to są etatowi pracownicy?

>> Ale mnie ogólnie chodzi o to, że nawet w przypadku redukcji ryzyka
>> fakapu korzyść z tego będzie mniejsza niż całkowity koszt
>> zastosowania metod formalnych.
>
> Jeśli korzyść z redukcji ryzyka fakapu będzie mniejsza od czegoś,
> czego nawet nie wyceniłeś,

Tzn. czego? Gdybyś chciał wprowadzać metody formalne to nie tylko koszt
tego byłby wyceniony z góry, ale też i potem firma by mierzyła ile to
kosztowało.

> to przyznajesz, że koszty fakapu są
> relatywnie niewielkie albo jego prawdopodobieństwo epsilonowe - ale
> przyznałeś też, że milionowe fakapy nie są niczym niezwykłym.
> Wychodzi mi to, co napisałem wcześniej - że fakapy są relatywnie
> tanie.

Nie "wychodzi", tylko nie bierzesz pod uwagę jakie mogą być koszty metod
formalnych.

Jeśli przykładowo masz aplikację, która bez fakapów zarobi w ciągu roku
5 milionów, ale ryzyko jest 20% że przez fakapy straci się te 5
milionów, i w tym 5%, że się narobi straty netto na 5 milionów, to można
powiedzieć, że koszty fakapu są duże, ale podjęcie ryzyka i uruchomienie
tej aplikacji nadal może być sensowną decyzją biznesową (nie mówię, że
koniecznie taką będzie, ale przynajmniej może być).

Jeśli zastosowanie metod formalnych zredukuje te prawdopodobieństwa do
odpowiednio 0.002% i 0.0005%, ale będzie kosztować 5 milionów, to można
powiedzieć, że się kompletnie nie opłaciło, chociaż fakapy są kosztowne.

No chyba że "relatywnie tanie" oznacza relatywnie do kosztów
zastosowania metod formalnych. W takim razie nie wykluczam, że nawet te
fakapy na setki milionów są relatywnie tanie.

> Ważne słowa: audyt, normy, sąd, działania korygujące.
>
> Czy te słowa występują w branży finansowej? Mówimy o warstwie
> technicznej.

Jak rozumiem takie rzeczy się owszem, dzieją, ale nie jest to coś, czym
się szczególnie interesuję.

Tylko że wcześniej mówiliśmy o konsekwencjach dla osoby podejmującej
decyzje, nie dla firmy. Jakie były konsekwencje dla osoby podejmującej w
Toyocie decyzje oo metodach rozwoju oprogramowania? Stanęła przed sądem
jako oskarżony? Straciła pracę? Popełniła sepukku?

> Działania korygujące wyglądają tak:
>
> http://www.automotive-eetimes.com/en/toyota-utilizes
-spark-pro-programming-language-in-ultra-low-defect-
software.html?cmp_id=7&news_id=222902902
>
> Panowie zauważyli, że:
>
> "[...] it enables lower development and maintenance efforts since the
> formal approach [...]"

Po pierwsze tam jest tylko napisane, że uruchomili "research project".
Jakie były wyniki tego "research" nie udało mi się znaleźć. Cynik mógłby
powiedzieć że był to ruch PR-owy w reakcji na wiadome problemy, żeby w
prasie nazwa firmy pojawiła się w sąsiedztwie słów "ultra low defect".

A jeśli chodzi o moją intuicję - choć przyznam, że jest to kolejna
rzecz, na której się nie znam, to działanie programu przekładającego
informację o wciśnięciu pedałów w samochodzie na jakieś sygnały
sterujące elementami mechanicznymi może być właśnie takim tematem, gdzie
akurat metody formalne się mogą opłacać.

> I ja właśnie dokładnie o tym - o rosnącym zainteresowaniu metodami
> formalnymi, które coraz częściej są postrzegane jako tańsza
> alternatywa dla testów. Przy okazji wspomniałem też o tym, że branża
> finansowa nie jest poziomem referencyjnym w temacie dbania o jakość
> produktów, chociaż wcale nie chciałem, aby stało się to głównym
> tematem tego wątku.

A ja pisałem o tym, że zainteresowanie jest głównie niszowe, w takich
właśnie niszach, w których może się to opłacać. Branża finansowa była
podana jako przykład na to, że nie zależy to tylko od wysokości realnych
lub potencjalnych strat.

I praktycznie w kwestii kolegi, który na grupie pytał o porady dotyczące
zastosowania takich metod w programie, który samodzielnie dłubie dla
jakiegośtam klienta, sprowadzałoby się to właśnie do "uważaj, bo może
się okazać, że to, co próbujesz zrobić kosztuje miliony dolarów". I tak,
uważam, że zarówno ten cały research project Toyoty jak i ewentualne
wdrożenie takiego czegoś do produkcji to jest skala kosztów co najmniej
milionów dolarów, ale Toyotę na to może być stać, bo jest Toyotą, a
kolega pytający na grupie - niekoniecznie.

do góry

On 29/03/2015 23:18, Maciej Sobczak wrote:
>
> W przeciwieństwie do Twojego przykładu z Knight Capital, gdzie
> regulatorzy uznali, że nie ma po co interweniować,

BTW, właśnie sprawdziłem i wygląda na to, że nie jest to prawda - poza
wszystkimi innymi stratami, Knight dostał dodatkowo 12-milionową karę od
SEC:
http://blog.klocwork.com/software-testing/lack-of-te
sting-cited-as-knight-capital-is-fined-12-million-fo
r-software-error/
http://www.bloomberg.com/bw/articles/2013-10-17/secs
-knight-capital-fine-adds-insult-to-injury

do góry

On Sun, 29 Mar 2015 14:18:54 -0700 (PDT), Maciej Sobczak
<s...@g...com> wrote:
> Mówimy o skandalu z Toyotą - zginęli ludzie. W przeciwieństwie do T=
> wojego przykładu z Knight Capital, gdzie regulatorzy uznali, że nie
ma =
> po co interweniować, z Toyotą uznali, że jak najbardziej należy int=

W przypadku Knight Capital pieniądze stracili wyłącznie akcjonariusze
firmy: klienci nic nie stracili, a podatnicy nie dotowali firmy.

RW

do góry

On Thu, 26 Mar 2015 00:19:47 +0100, Andrzej Jarzabek
<a...@g...com> wrote:
> dowodzenie jest bardzo kosztowne - jest uważane za nieopłacalne
nawet

Dowód formalny nie pomoże na np. zagubienie przecinka i napisanie 314
zamiast 3.14.

Testy (jednostkowe) i audyt kodu mogą, ale nie muszą.

Trzecia droga to OC. Finansowa polisa na wypadek strat wywołanych
błędem.

Bo jak nie masz zoo to, teoretycznie, może być bardzo nieciekawie.

No i jeszcze: jeżeli zleceniodawca uważa że to robota dla jednego
człowieka... to albo jest głupi, albo to nie jest aż tak makabryczne
odpowiedzialne.

do góry

On Thu, 26 Mar 2015 22:29:57 +0100, Andrzej Jarzabek
<a...@g...com> wrote:
> co można zrobić żeby udowodnuć jego poprawność i ile to będzie
kosztowało?

Dodam - a jak sprawdzić poprawność dowodu? Tzn. że w czasie
udowadniania nie popełniono pomyłki?

W matematyce też "udowadniania" różne rzeczy, a że potem znajdowano
błąd w dowodach...

do góry

On Fri, 27 Mar 2015 02:57:24 -0700 (PDT), g...@g...com
wrote:
> To jest akurat rzecz podstawowa: wystarczy pokazać, że każdy krok
dow=
> odu
> wynika logicznie z tez dowiedzionych wcześniej, albo przyjętych
przez n=
> as
> aksjomatów, w oparciu o uznawane przez nas reguły wnioskowania
> (które uważamy za oczywiste).

Marzyciel z ciebie.

do góry