W dniu piątek, 27 marca 2015 10:06:11 UTC+1 użytkownik Maciej Sobczak napisał:
>
> > 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).

Tutaj akurat widzę pomylenie pojęć. Testowanie to uruchamianie
programu z założeniem sprawdzenia, jak się zachowuje w określonych
okolicznościach. Nie wiem, dlaczego programów napisanych w C++
miałoby się nie dać uruchomić z zamiarem sprawdzenia, jak się zachowuje
w określonych okolicznościach.

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

To jest ciekawe pytanie: jakie znacie systemy stworzone z myślą
o dowodzeniu poprawności napisanych w nich programów?

I przy okazji kilka ciekawostek, które ostatnio przebiegły twittera:

"What if you could write a test for a problem and have your compiler automatically
return a correct implementation?":
http://blogs.teamb.com/craigstuntz/2014/07/07/38818/

Microsoft (chyba wczoraj) wypuścił źródła systemu Z3 używanego w w/w
artykule: github.com/Z3Prover/z3

Dowód sprzeczności w systemie Coq: https://github.com/clarus/falso

> Ćwiczenie logiczne: jeżeli ktoś twierdzi, że testuje swój program,
> to ja poproszę o *dowód*, że testowanie jest kompletne.

Na tym chyba polega istotowa różnica między dowodem a testowaniem,
że dowód wyczerpuje wszystkie możliwości, a testowanie nie.
"Kompletne testowanie" byłoby właśnie -- po prostu -- dowodem.

do góry

On Friday, March 27, 2015 at 10:57:26 AM UTC+1, g...@g...com wrote:
> 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
Właśnie o tym pisałem. Poprawność dowodu, to też jego poprawność w
odzwierciedlaniu oryginalnego zadania.

do góry

W dniu piątek, 27 marca 2015 12:24:48 UTC+1 użytkownik M.M. napisał:
> On Friday, March 27, 2015 at 10:57:26 AM UTC+1, g...@g...com wrote:
> > 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
> Właśnie o tym pisałem. Poprawność dowodu, to też jego poprawność w
> odzwierciedlaniu oryginalnego zadania.

W takim razie zgoda -- tego rodzaju "poprawność" jest niemożliwa do uzyskania.
Należy jednak mieć na uwadze, że z formalnego punktu widzenia poprzez
"poprawność" dowodu rozumie się to, czy każdy krok jest zgodny z regułami,
natomiast w tym przypadku raczej należałoby użyć słowa "adekwatność"
(na przykład teza Churcha-Turinga postuluje adekwatność maszyny Turinga
jako modelu ujmującego intuicyjne rozumienie obliczalności)

Jednak z drugiej strony jeśli mamy na przykład dowód indukcyjny twierdzenia,
że funkcja "append" zdefiniowana (dajmy na to w czymś haskelopodobnym) jako

append [] y = y
append (h:t) y = h:(append t y)

jest operatorem łącznym, tzn dla dowolnych skończonych list a, b, c
append (append a b) c === append a (append b c)

to tak naprawdę trudno jest to kwestionować i podważać, tzn. albo uznajemy
regułę indukcji, i wtedy musimy uznać dowód za poprawny, albo jej nie uznajemy,
i obawiamy się, że "mogą istnieć takie listy, dla których append wcale
nie będzie się zachowywał jako operator łączny" -- choć byłoby czymś
szokującym, gdyby ktoś był w stanie podać pozbawione błędów rozumowanie,
które pozwalałoby taki obiekt skonstruować. Tym bardziej trudno byłoby
tutaj sformułować zarzut nieadekwatności, bo nie za bardzo można wskazać
jakąś zewnętrzną dziedzinę problemową, do której mielibyśmy odnosić
dowód

(a przy okazji jak kogoś ciekawi, to znajdzie ten dowód w notatkach
http://www.cl.cam.ac.uk/teaching/Lectures/funprog-jr
h-1996/all.pdf
na stronie 86)

do góry

> Tutaj akurat widzę pomylenie pojęć. Testowanie to uruchamianie
> programu z założeniem sprawdzenia, jak się zachowuje w określonych
> okolicznościach.

Tak. Można nawet jakiegoś buga tak znaleźć.

> Nie wiem, dlaczego programów napisanych w C++
> miałoby się nie dać uruchomić z zamiarem sprawdzenia, jak się zachowuje
> w określonych okolicznościach.

Da się. Ale nie da się stwierdzić, czy te sprawdzone okoliczności wyczerpują możliwe
stany i zachowania sprawdzanego programu, adekwatnie do wszystkich możliwich sposobów
przyszłego użycia.

Przykładowo, da się napisać test, który "sprawdza" funkcję sortującą i zapewne ktoś
taki test napisał w Javie dla funkcji napisanej dekadę temu. Dało się to napisać i
uruchomić.

Ale rzeczona funkcja nadal była zje-banana, co raczej rzuca cień i rysę na taką
metodę.

> To jest ciekawe pytanie: jakie znacie systemy stworzone z myślą
> o dowodzeniu poprawności napisanych w nich programów?

SPARK?

> I przy okazji kilka ciekawostek, które ostatnio przebiegły twittera:
>
> "What if you could write a test for a problem and have your compiler automatically
return a correct implementation?":

Fajne. Zwłaszcza jak ktoś napisze zły test. Będzie miał wtedy złą implementację
pasującą idealnie do tego złego testu.

Spuszczamy to z wodą.

Podobnie jak automaty, który generują testy z implementacji. To jest taka sama
ściema. Implementacja i test to są dwa *niezależne* artefakty, które się uzupełniają
właśnie dzięki temu, że są niezależne. Jak ktoś generuje jedno z drugiego, to równie
dobrze mógłby jednego w ogóle nie robić.
Np. umówmy się, że wtedy nie robimy testów. To bardzo popularna metoda jest.

> Na tym chyba polega istotowa różnica między dowodem a testowaniem,
> że dowód wyczerpuje wszystkie możliwości, a testowanie nie.
> "Kompletne testowanie" byłoby właśnie -- po prostu -- dowodem.

Dokładnie. Stąd właśnie bierze się potencjalny zysk z użycia dowodów, które w
porównaniu do kompletnych testów mogą być tańsze. Bo to, że dowody mogą być droższe
od niekompletnych testów, to jest argument dla Dilberta.

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

do góry

W dniu piątek, 27 marca 2015 15:12:10 UTC+1 użytkownik Maciej Sobczak napisał:

> > Nie wiem, dlaczego programów napisanych w C++
> > miałoby się nie dać uruchomić z zamiarem sprawdzenia, jak się zachowuje
> > w określonych okolicznościach.
>
> Da się. Ale nie da się stwierdzić, czy te sprawdzone okoliczności wyczerpują
możliwe stany i zachowania sprawdzanego programu, adekwatnie do wszystkich możliwich
sposobów przyszłego użycia.

Da się z łatwością stwierdzić, że zazwyczaj nie wyczerpują.

> Przykładowo, da się napisać test, który "sprawdza" funkcję sortującą i zapewne ktoś
taki test napisał w Javie dla funkcji napisanej dekadę temu. Dało się to napisać i
uruchomić.
>
> Ale rzeczona funkcja nadal była zje-banana, co raczej rzuca cień i rysę na taką
metodę.

Mnie się zdaje, że to w ogólności jest "cieńka" metoda. Tym bardziej,
że wielu ideologów pisania testów mówią, że "im więcej, tym lepiej"
i że "testy nie muszą być elegancko napisane" -- problem jest taki,
że testy również potrafią czynić pewne założenia, które nie są kluczowe
z perspektywy projektu, a których zmiana w projekcie sprawi, że słita
testowa stanie się bezużyteczna.

> > I przy okazji kilka ciekawostek, które ostatnio przebiegły twittera:
> >
> > "What if you could write a test for a problem and have your compiler
automatically return a correct implementation?":
>
> Fajne. Zwłaszcza jak ktoś napisze zły test. Będzie miał wtedy złą implementację
pasującą idealnie do tego złego testu.
>
> Spuszczamy to z wodą.

A co jeśli ktoś napisze zły test i złą implementację? Taki sam klops.
Jednak artykuł w gruncie rzeczy nie opisywał tego, o czym mówił
ten nagłówek, tylko po prostu pewną odmianę programowania
deklaratywnego opartą o microsoftowy system.

> Podobnie jak automaty, który generują testy z implementacji. To jest taka sama
ściema. Implementacja i test to są dwa *niezależne* artefakty, które się uzupełniają
właśnie dzięki temu, że są niezależne. Jak ktoś generuje jedno z drugiego, to równie
dobrze mógłby jednego w ogóle nie robić.
> Np. umówmy się, że wtedy nie robimy testów. To bardzo popularna metoda jest.

Tzn. generowanie testów z implementacji rzeczywiście brzmi idiotycznie.
Jednak w drugą stronę to nie całkiem zachodzi. Jeżeli mamy system, który
na podstawie testów potrafi wygenerować sensowną implementację, to szacun.

> > Na tym chyba polega istotowa różnica między dowodem a testowaniem,
> > że dowód wyczerpuje wszystkie możliwości, a testowanie nie.
> > "Kompletne testowanie" byłoby właśnie -- po prostu -- dowodem.
>
> Dokładnie. Stąd właśnie bierze się potencjalny zysk z użycia dowodów, które w
porównaniu do kompletnych testów mogą być tańsze. Bo to, że dowody mogą być droższe
od niekompletnych testów, to jest argument dla Dilberta.

Ja jednak będę trwał na stanowisku, że testy są z założenia niekompletne,
bo obejmują pewne przypadki jednostkowe. I testy jako takie mają pewną
wartość. Podobnie jak program QuickCheck.

I owszem, zgodzę się, że fajniej jest mieć dowody poprawności, kiedy
tylko się da (choć nie wiem, czy akurat w logice Hoare'a), ale jedno
nie wyklucza drugiego. Tak jak fajnie np. w podręczniku do matematyki
mieć nie tylko definicje, twierdzenia i dowody, ale również przykłady.

do góry

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.

do góry

On Friday, March 27, 2015 at 1:21:22 PM UTC+1, g...@g...com wrote:
> W dniu piątek, 27 marca 2015 12:24:48 UTC+1 użytkownik M.M. napisał:
> > On Friday, March 27, 2015 at 10:57:26 AM UTC+1, g...@g...com wrote:
> > > 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
> > Właśnie o tym pisałem. Poprawność dowodu, to też jego poprawność w
> > odzwierciedlaniu oryginalnego zadania.
>
> W takim razie zgoda -- tego rodzaju "poprawność" jest niemożliwa do uzyskania.
> Należy jednak mieć na uwadze, że z formalnego punktu widzenia poprzez
> "poprawność" dowodu rozumie się to, czy każdy krok jest zgodny z regułami,
> natomiast w tym przypadku raczej należałoby użyć słowa "adekwatność"
> (na przykład teza Churcha-Turinga postuluje adekwatność maszyny Turinga
> jako modelu ujmującego intuicyjne rozumienie obliczalności)

Mój (hipotetyczny) klient zamawia najlepszy program do gry w
szachy o łącznym rozmiarze kodu i danych nie większym niż 1MB. Napisałem
taki program. Jak mam przeprowadzić dowód, że nie istnieje w
ramach tego rozmiaru lepszy program?



>
> Jednak z drugiej strony jeśli mamy na przykład dowód indukcyjny twierdzenia,
> że funkcja "append" zdefiniowana (dajmy na to w czymś haskelopodobnym) jako
>
> append [] y = y
> append (h:t) y = h:(append t y)
>
> jest operatorem łącznym, tzn dla dowolnych skończonych list a, b, c
> append (append a b) c === append a (append b c)
>
> to tak naprawdę trudno jest to kwestionować i podważać, tzn. albo uznajemy
> regułę indukcji, i wtedy musimy uznać dowód za poprawny, albo jej nie uznajemy,
> i obawiamy się, że "mogą istnieć takie listy, dla których append wcale
> nie będzie się zachowywał jako operator łączny" -- choć byłoby czymś
> szokującym, gdyby ktoś był w stanie podać pozbawione błędów rozumowanie,
> które pozwalałoby taki obiekt skonstruować. Tym bardziej trudno byłoby
> tutaj sformułować zarzut nieadekwatności, bo nie za bardzo można wskazać
> jakąś zewnętrzną dziedzinę problemową, do której mielibyśmy odnosić
> dowód
>
> (a przy okazji jak kogoś ciekawi, to znajdzie ten dowód w notatkach
> http://www.cl.cam.ac.uk/teaching/Lectures/funprog-jr
h-1996/all.pdf
> na stronie 86)

do góry

W dniu piątek, 27 marca 2015 16:00:39 UTC+1 użytkownik g...@g...com napisał:

> Mnie się zdaje, że to w ogólności jest "cieńka" metoda. Tym bardziej,
> że wielu ideologów pisania testów mówią, że "im więcej, tym lepiej"
> i że "testy nie muszą być elegancko napisane" -- problem jest taki,
> że testy również potrafią czynić pewne założenia, które nie są kluczowe
> z perspektywy projektu, a których zmiana w projekcie sprawi, że słita
> testowa stanie się bezużyteczna.

Tak. I na tej podstawie można też podważyć stosowanie takich artefaktów do testowania
regresji. Może być tak, że po zmianie w implementacji i wprowadzeniu do niej bugów
stary test nadal będzie przechodził, bo nie testuje nowo powstałych osobliwości.

Testów nie da się pisać na masę, chyba że ktoś chce uprawiać poprawność tzw.
statystyczną. To też ma jakąś wartość, ale trzeba wiedzieć, gdzie.

> A co jeśli ktoś napisze zły test i złą implementację? Taki sam klops.

I te rzeczy były pisane przez niezależnych wykonawców? To wtedy prawdopodobieństwo
znalezienia niezgodności jest bardzo wysokie i wiadomo, że co najmniej jedno z dwóch
jest zwalone. Tej efektywności nie ma gdy się robi jedno z drugiego (tu z pogardą
spoglądamy również na TDD).

Podobno w praktyce wychodzi 50-50, więc tym bardziej nie należy traktować jednego z
tych artefaktów jako nadrzędnego.

> Jednak artykuł w gruncie rzeczy nie opisywał tego, o czym mówił
> ten nagłówek, tylko po prostu pewną odmianę programowania
> deklaratywnego opartą o microsoftowy system.

Jasne. W takim kontekście jest to bardzo ciekawe. Szkoda tylko, że niepraktyczne.

> Tzn. generowanie testów z implementacji rzeczywiście brzmi idiotycznie.
> Jednak w drugą stronę to nie całkiem zachodzi. Jeżeli mamy system, który
> na podstawie testów potrafi wygenerować sensowną implementację, to szacun.

Szacun dla systemu. Ale nadal niepraktyczne.

Taki system zmusza autora testu do takiego sformułowania testu, żeby z jego formuły
wynikała kompletna implementacja. Tzn. albo test musi być wyczerpujący albo musi być
tak skonstruowany, żeby *nie dało się* z niego zrobić niekompletnej implementacji.
Np. napisz test, który sprawdza funkcję sort - ale napisz go tak, żeby po
wygenerowaniu implementacji z tego testu, każdy inny test też przechodził.
I jeszcze udowodnij, że tak jest.

Wysiłek intelektualny z tym związany jest porównywalny z napisaniem tej funkcji. I
udowodnienia, że jest poprawna.

To jest jak ze ściskaniem plasteliny w dłoni - po prostu wylezie z innej strony a jej
objętość się nie zmniejszy.

> Ja jednak będę trwał na stanowisku, że testy są z założenia niekompletne,
> bo obejmują pewne przypadki jednostkowe.

Mogą obejmować wszystkie klasy równoważności (albo w ogóle być wyczerpujące w sensie
przestrzeni wejść). Ale znalezienie wszystkich klas równoważności jest tak samo
trudne, jak dowód z pominięciem testów. A testy wyczerpujące to tylko dla
najprostszych funkcji logicznych można napisać przed zejściem.

> I testy jako takie mają pewną
> wartość.

Tak. Oraz cenę.

> I owszem, zgodzę się, że fajniej jest mieć dowody poprawności, kiedy
> tylko się da (choć nie wiem, czy akurat w logice Hoare'a), ale jedno
> nie wyklucza drugiego. Tak jak fajnie np. w podręczniku do matematyki
> mieć nie tylko definicje, twierdzenia i dowody, ale również przykłady.

Tak. Ale dowodem można uzasadnić zmniejszenie ilości testów. Tak jak w książce do
matematyki nie trzeba podawać wyczerpujacych przykładów, wystarczy podać te
ilustracyjne. Wtedy książka może mieć mniej kartek i może być tańsza.

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

do góry

W dniu sobota, 28 marca 2015 05:04:04 UTC+1 użytkownik M.M. napisał:

> > W takim razie zgoda -- tego rodzaju "poprawność" jest niemożliwa do uzyskania.
> > Należy jednak mieć na uwadze, że z formalnego punktu widzenia poprzez
> > "poprawność" dowodu rozumie się to, czy każdy krok jest zgodny z regułami,
> > natomiast w tym przypadku raczej należałoby użyć słowa "adekwatność"
> > (na przykład teza Churcha-Turinga postuluje adekwatność maszyny Turinga
> > jako modelu ujmującego intuicyjne rozumienie obliczalności)
>
> Mój (hipotetyczny) klient zamawia najlepszy program do gry w
> szachy o łącznym rozmiarze kodu i danych nie większym niż 1MB. Napisałem
> taki program. Jak mam przeprowadzić dowód, że nie istnieje w
> ramach tego rozmiaru lepszy program?

To akurat nie jest problem metody dowodowej, tylko nieprecyzyjnej
specyfikacji. Co to znaczy,że "w ramach określonego rozmiaru program
jest lepszy od innego programu"?

Zresztą cechy użytkowe nie są czymś, co dowodzi się formalnie
(bo są subiektywne). Formalnie chcemy dowodzić raczej pewnych
inwariantów -- że na przykład w programie wielowątkowym nie dojdzie
do sytuacji dead-locku (klasyczne zastosowane logik temporalnych),
że dla określonej klasy danych wejściowych program się zatrzyma,
że zużycie zasobów w czasie działania programu będzie ograniczona
określoną funkcją od czasu działania i rozmiaru danych wejściowych
itd.

do góry

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

do góry