> > > Sugerujesz że są programy które po podaniu specyfikacji wejścia i wyników oraz
podaniu niemienników dowodzą automatycznie poprawności?
> Nie wiem jak to zabrzmialo, ale nic takiego nie zamierzałem sugerować.
> Po prostu ręczne nafaszerowanie programu asercjami, to pomocna metoda
> w usuwaniu błędów.

Pomysł z asercjami jest chyba tym co mi jest potrzebne. Dzięki.

do góry

On 25.03.2015 20:05, j...@p...onet.pl wrote:
>> A zleceniodawca wymaga formalnego dowodu poprawności programu?
>
> nie wymaga, ale jeśli mój algorytm będzie niepoprawny to zostanie
> poważnie naruszona reputacja jego firmy

Wygraliście przetarg PKW na wybory prezydenckie?

;-)

pzdr
bartekltg

do góry

On 25/03/2015 20:06, j...@p...onet.pl wrote:
>>>> Sugerujesz że są programy które po podaniu specyfikacji wejścia i wyników oraz
podaniu niemienników dowodzą automatycznie poprawności?
>> Nie wiem jak to zabrzmialo, ale nic takiego nie zamierzałem sugerować.
>> Po prostu ręczne nafaszerowanie programu asercjami, to pomocna metoda
>> w usuwaniu błędów.
>
> Pomysł z asercjami jest chyba tym co mi jest potrzebne. Dzięki.

Tyle że asercje nie są formalnym dowodem, a jedynie kolejnym rodzajem testu.

do góry

On 25/03/2015 20:05, j...@p...onet.pl wrote:
>> A zleceniodawca wymaga formalnego dowodu poprawności programu?
>
> nie wymaga, ale jeśli mój algorytm będzie niepoprawny to zostanie
> poważnie naruszona reputacja jego firmy

Nie znam się na algorytmach i ich dowodzeniu, ale mogę powiedzieć tyle,
że normalną praktyką w przemyśle jest testowanie a nie dowodzenie, bo
dowodzenie jest bardzo kosztowne - jest uważane za nieopłacalne nawet
tam, gdzie wchodzą w grę wielomilionowe straty (np. w finansach), a
zaczyna się je stosować AFAIK gdzieś w okolicach oprogramowania pojazdów
kosmicznych - duże potencjalne straty, stosunkowo mała liczba linii kodu.

Poprawność programu praktycznie nigdy nie jest kwestią 100% pewności a
zawsze jest kwestią zarządzania ryzykiem. Zawsze jest pewne
prawdopodobieństwo, że program zawiedzie powodując jakieś straty - nawet
jeśli formalnie udowodniłeś jego poprawność - i zawsze jest pytanie, ile
czasu, pieniędzy i innych zasobów można poświęcić, żeby to ryzyko o
ileśtam zredukować.

Trochę piszę oczywistości, ale piszę to dlatego, że skoro twój
zleceniodawca wymaga, żebyś robił to sam, to być może inne względy
(zachowanie tajemnicy? koszty?) są dla niego ważniejsze niż ryzyko
utraty reputacji na wskutek błędnego działania programu. Druga możliwość
jest oczywiście taka, że nie jest tego świadomy.

do góry

> Nie znam się na algorytmach i ich dowodzeniu, ale mogę powiedzieć tyle,
> że normalną praktyką w przemyśle jest testowanie a nie dowodzenie,

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.

> bo
> dowodzenie jest bardzo kosztowne - jest uważane za nieopłacalne

Nie. Zainteresowanie dowodzeniem rośnie właśnie dlatego, że jest tańsze. Może być
nawet dużo tańsze.

> nawet
> tam, gdzie wchodzą w grę wielomilionowe straty (np. w finansach),

W finansach nie ma strat. Albo się "traci" coś, czego nigdy nie było (wtedy nie ma
strat), albo można to stosunkowo łatwo odkręcić przez reklamacje i wtedy (relatywnie)
też nie ma strat.

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.

> a
> zaczyna się je stosować AFAIK gdzieś w okolicach oprogramowania pojazdów
> kosmicznych - duże potencjalne straty, stosunkowo mała liczba linii kodu.

Dowody da się automatyzować. Przy dużej liczbie linii kodu nie masz szans go pokryć
testami, natomiast nadal masz szansę robić dowody. Stąd też to rosnące
zainteresowanie.

> Poprawność programu praktycznie nigdy nie jest kwestią 100% pewności a
> zawsze jest kwestią zarządzania ryzykiem.

Tak.

> Trochę piszę oczywistości,

Nie.

> ale piszę to dlatego, że skoro twój
> zleceniodawca wymaga, żebyś robił to sam, to być może inne względy
> (zachowanie tajemnicy? koszty?) są dla niego ważniejsze niż ryzyko
> utraty reputacji na wskutek błędnego działania programu. Druga możliwość
> jest oczywiście taka, że nie jest tego świadomy.

Stawiam na drugą. Jeśli ten program jest naprawdę taki ważny, to zleceniodawca
powinien zlecić wszystkie metody weryfikacji jakie da się zastosować - review, testy
i dowody. I normalne standardy jakości wymagają, żeby każda z tych metod angażowała
*niezależną* osobę do jej przeprowadzenia (nikt nie widzi własnych błędów).
Stąd też bzdurą jest oczekiwanie, że wszystko zrobi jeden wykonawca.

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

do góry

On 26.03.2015 15:03, Maciej Sobczak wrote:
>
>
>
> Stawiam na drugą. Jeśli ten program jest naprawdę taki ważny, to
> zleceniodawca powinien zlecić wszystkie metody weryfikacji jakie da się
> zastosować - review, testy i dowody. I normalne standardy jakości
> wymagają, żeby każda z tych metod angażowała *niezależną* osobę do jej
> przeprowadzenia (nikt nie widzi własnych błędów).
> Stąd też bzdurą jest oczekiwanie, że wszystko zrobi jeden wykonawca.

No ale się nie da, bo na zintegrowany system koordynacji sił
przeciwlotniczych i przeciwrakietowych oraz wczesnego ostrzegania
97% punktów do przetargu jest z ceny.
;-)

pzdr
bartekltg

do góry

On 26/03/2015 15:03, Maciej Sobczak wrote:
>
>> Nie znam się na algorytmach i ich dowodzeniu, ale mogę powiedzieć
>> tyle, że normalną praktyką w przemyśle jest testowanie a nie
>> dowodzenie,
>
> 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.

>> bo dowodzenie jest bardzo kosztowne - jest uważane za nieopłacalne
>
> Nie. 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ć.

>> nawet tam, gdzie wchodzą w grę wielomilionowe straty (np. w
>> finansach),
>
> W finansach nie ma strat. Albo się "traci" coś, czego nigdy nie było
> (wtedy nie ma strat), albo można to stosunkowo łatwo odkręcić przez
> reklamacje i wtedy (relatywnie) też nie ma strat.
>
> 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.

>> a zaczyna się je stosować AFAIK gdzieś w okolicach oprogramowania
>> pojazdów kosmicznych - duże potencjalne straty, stosunkowo mała
>> liczba linii kodu.
>
> Dowody da się automatyzować. Przy dużej liczbie linii kodu nie masz
> szans go pokryć testami, natomiast nadal masz szansę robić dowody.
> Stąd też to rosnące zainteresowanie.

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?

do góry

On Thursday, March 26, 2015 at 10:29:57 PM UTC+1, Andrzej Jarzabek wrote:
> 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?
Myślę że w praktyce w ogóle nie ma możliwości przeprowadzenia takiego
dowodu, nawet dla mniejszych programów. Jak udowodnić, że w dowodzie
nie ma błędu?
Pozdrawiam

do góry

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

do góry

> Myślę że w praktyce w ogóle nie ma możliwości przeprowadzenia takiego
> dowodu, nawet dla mniejszych programów. Jak udowodnić, że w dowodzie
> nie ma błędu?

To jest akurat rzecz podstawowa: wystarczy pokazać, że każdy krok dowodu
wynika logicznie z tez dowiedzionych wcześniej, albo przyjętych przez nas
aksjomatów, w oparciu o uznawane przez nas reguły wnioskowania
(które uważamy za oczywiste).

Walidacja dowodu jest zabiegiem bardzo prostym -- z pewnością
o wiele prostszym, niż znalezienie dowodu.

Oczywiście pewien problem natury epistemicznej wiąże się ze sformułowaniem
odpowiedniej listy aksjomatów, które miałyby odzwierciedlać rozważany
przez nas problem

do góry