W dniu 2015-03-28 10:54, M.M. pisze:

>> 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),
> Nie słyszałem o logice temporalnej. Może się mylę, ale to się
> wydaje łatwe. Dla mnie taki dowód sprowadza się do tego, aby
> wszystkie pary kodu, który może wykonać się równolegle, były
> opatrzone semaforami w tej samej kolejności w sensie wykonania i
> w odwrotnej kolejności (też w sensie wykonania).

Samo opatrzenie semaforami to często za mało by uniknąć dead-locka,
jeśli sekwencji chronionych jest więcej niż jedna. Dodatkowo dochodzi
jeszcze dbanie o integralność danych itp rzeczy.


--
Kaczus
http://kaczus.ppa.pl/art/liczbyzmiennoprzecinkowe,19
.html

do góry

W dniu piątek, 27 marca 2015 10:57:26 UTC+1 użytkownik g...@g...com napisał:
> > 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).
>

nie jestem pewien czy to wystarczy.. czasem moze nawet dosyc czesto moze okazac sie
ze
mio ze te wnioskowania byly poprawne to
ogolnie problem wynika z przeoczenia pewnych
pobocznych czynników

innymi slowy mi wyglada na to ze dowody sa
rowniez czesciowe tak samo jak testy ;/

> 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

W dniu poniedziałek, 30 marca 2015 00:59:51 UTC+2 użytkownik Andrzej Jarzabek
napisał:

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

Faktycznie. Na szczęście koledzy pomogli:

http://www.wsj.com/articles/SB1000087239639044424690
4577572752865497064

"a group of financial firms injecting $400 million to keep Knight Capital Group Inc.
afloat"

Bo jeśli się dobrze zastanowić, to te stracone 400 baniek nie zniknęło w takim sensie
jak zabity człowiek, czy nawet rozbity samochód, tylko zmieniło miejsce pobytu, bo
strata Rysia jest zyskiem Krzysia. Dlatego rynek jako całość jest zainteresowany tym,
żeby to trwało dalej.

W przypadku fakapów z jeszcze większą ilością zer (niezależnie od tego, jaką
przyczynę mają takie fakapy, bo nie musi być techniczna), pomocną dłoń wyciągają całe
rządy albo nawet unie międzypaństwowe, a sponsorami są podatnicy. Przykłady
praktyczne opisano w prasie.

I gramy dalej.

To jest właśnie ten brak presji na szukanie lepszych rozwiązań. Ma być akceptowalna
jakość za akceptowalną cenę i tak właśnie jest, bo per saldo jest na plus a skoro
tak, to wdrażanie nowych metod się nie opłaca.
Co ciekawe, razem to napisaliśmy, tylko innymi słowami.

Po co ciągniemy ten wątek, skoro od początku się ze sobą zgadzamy?

Jeśli chodzi o wsadzanie programistów do więzień, to specjalnie napisałem dwa punkty:

1. osobiste konsekwencje
2. osobiste korzyści

żeby pokazać jak one działają *razem*. To jest kij i marchewka i razem działają
inaczej w różnych branżach. Bo o ile programistów nigdzie się nie wsadza, to wysokie
premie za zrobienie czegoś szybciej niż sąsiad w pewnych branżach są a w innych ich
nie ma. I dlatego, te dwa punkty *razem* tworzą różny poziom presji na stosowanie i
szukanie różnych metod w różnych branżach. Po co to rozstrząsać, skoro to zostało
opisane przez behawiorystów już dawno temu?

Porozmawiajmy lepiej o programowaniu.

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

do góry

W dniu poniedziałek, 30 marca 2015 09:49:49 UTC+2 użytkownik slawek napisał:
> 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.

Z ciekawości zapytam: jakie masz doświadczenie z formalnym dowodzeniem
twierdzeń?

do góry

On Monday, March 30, 2015 at 10:18:41 AM UTC+2, Tomasz Kaczanowski wrote:
> W dniu 2015-03-28 10:54, M.M. pisze:
>
> >> 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),
> > Nie słyszałem o logice temporalnej. Może się mylę, ale to się
> > wydaje łatwe. Dla mnie taki dowód sprowadza się do tego, aby
> > wszystkie pary kodu, który może wykonać się równolegle, były
> > opatrzone semaforami w tej samej kolejności w sensie wykonania i
> > w odwrotnej kolejności (też w sensie wykonania).
>
> Samo opatrzenie semaforami to często za mało by uniknąć dead-locka,
> jeśli sekwencji chronionych jest więcej niż jedna.
No oczywiście. Samo opatrzenie to nawet może spowodować dead-locka.
Chodzi o kolejność. Mamy cokolwiek, semafory, sekcje chronione, itd
blokujące dostęp do zasobów, niech się one nazywają A,B,C.

Jeśli jeden fragment jest opatrzony kolejnością
A
B
kod
B
A

A drugi
B
A
kod
A
B

To może dojść do dead-locka. Gdy kolejność zawsze będzie od A do C, to
nigdy nie dojdzie do dead-locka. Ja wiem że czasami jest tak:

Pierwszy wątek
A
B
kod
B
A

Drugi wątek
B
kod 1
A
kod 2
A
B

Aż prosi się, żeby kod 1 był opatrzony tylko jednym semaforem, ponieważ
można lepiej wykorzystać zasoby systemu. Niestety to gorzi dead-lockiem.
Trzeba w jednym z przypadków zmienić kolejność.

Pozdrawiam


> Dodatkowo dochodzi
> jeszcze dbanie o integralność danych itp rzeczy.
Tutaj zasada też jest prosta. Jeśli na danych pracuję więcej niż jeden
wątek i jeśli przynajmniej jeden wątek może zmodyfikować dane, to
powinno być objęte sekcją krytyczną, semaforem, itd. Czasami stosuje
się rozwiązana lockless, pomimo że wiele wątków pisze pod te same
adresy pamięci - to już w ogóle masakra :)

Pozdrawiam

>
>
> --
> Kaczus
> http://kaczus.ppa.pl/art/liczbyzmiennoprzecinkowe,19
.html

do góry

On 30/03/2015 11:15, Maciej Sobczak wrote:
> W dniu poniedziałek, 30 marca 2015 00:59:51 UTC+2 użytkownik Andrzej
> Jarzabek napisał:
>
>> 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:
>
> Faktycznie. Na szczęście koledzy pomogli:
>
> http://www.wsj.com/articles/SB1000087239639044424690
4577572752865497064
>
> "a group of financial firms injecting $400 million to keep Knight
> Capital Group Inc. afloat"

Przecież nie charytatywnie, tylko żeby przejąć firmę. Myślisz, że gdyby
taka Toyota stanęła na skraju bankructwa z powodu serii wyjątkowo
katastrofalnych usterek, to by nikt się nie pokusił o kupno akcji za bezcen?

> Bo jeśli się dobrze zastanowić, to te stracone 400 baniek nie
> zniknęło w takim sensie jak zabity człowiek, czy nawet rozbity
> samochód, tylko zmieniło miejsce pobytu, bo strata Rysia jest zyskiem
> Krzysia. Dlatego rynek jako całość jest zainteresowany tym, żeby to
> trwało dalej.

Fantazjujesz. Przed chwilą jak pisałem o tym, że te firmy zajmują się
zarabianiem pieniędzy, to ofukałeś mnie, że piszę banały, a teraz jakbyś
tego nie rozumiał. Zarabianie pieniędzy polega na tym, że działania
firmy nakierowane są na zyski własne, a nie innych graczy. Inwestorzy są
zainteresowani tym, żeby zyskiwać na firmie, w którą zainwestowali, a
nie żeby zyskiwał jakiś Krzyś.

A na rozbijających się samochodach Toyoty zyskuje Ford czy inny Fiat.

> W przypadku fakapów z jeszcze większą ilością zer (niezależnie od
> tego, jaką przyczynę mają takie fakapy, bo nie musi być techniczna),
> pomocną dłoń wyciągają całe rządy albo nawet unie międzypaństwowe, a
> sponsorami są podatnicy. Przykłady praktyczne opisano w prasie.

No jasne, bo nigdy się nie zdarzyło, żeby państwo pomagało przemysłowi
motoryzacyjnemu. Albo np. kosmicznemu.

> To jest właśnie ten brak presji na szukanie lepszych rozwiązań. Ma
> być akceptowalna jakość za akceptowalną cenę i tak właśnie jest, bo
> per saldo jest na plus a skoro tak, to wdrażanie nowych metod się nie
> opłaca. Co ciekawe, razem to napisaliśmy, tylko innymi słowami.

Nie zgodzę się, jak najbardziej jest presja na szukanie lepszych
rozwiązań i wdrażanie nowych metod. Tylko że nie ma za bardzo przesłanek
na to, że metody formalne są lepszym rozwiązaniem.


> Po co ciągniemy ten wątek, skoro od początku się ze sobą zgadzamy?
>
> Jeśli chodzi o wsadzanie programistów do więzień, to specjalnie
> napisałem dwa punkty:
>
> 1. osobiste konsekwencje 2. osobiste korzyści
>
> żeby pokazać jak one działają *razem*. To jest kij i marchewka i
> razem działają inaczej w różnych branżach. Bo o ile programistów
> nigdzie się nie wsadza, to wysokie premie za zrobienie czegoś
> szybciej niż sąsiad w pewnych branżach są a w innych ich nie ma. I
> dlatego, te dwa punkty *razem* tworzą różny poziom presji na
> stosowanie i szukanie różnych metod w różnych branżach. Po co to
> rozstrząsać, skoro to zostało opisane przez behawiorystów już dawno
> temu?

Ale te presje też wynikają z tego, że na opóżnieniach traci się
pieniądze. Jeśli wysiłek włożony w opracowanie i zastosowanie metod
formalnych kosztuje pół miliona, ale generuje opóźnienie powodujące, że
zamiast pięciu milionów nasza poprawna aplikacja zarobi półtora, to
znaczy, że koszt zastosowania metod formalnych wynosi cztery miliony, a
nie pół miliona. I o to również mi chodziło kiedy wyrażałem
przypuszczenie, że metody formalne są zbyt kosztowne, żeby być opłacalnymi.

Poza tym w instytucjach finansowych oprócz typowych aplikacji front
office, o których dyskutowaliśmy, jest wiele innych rodzajów
oprogramowania, gdzie nie ma wcale takiej motywacji, a co za tym idzie
presji na szybkie wdrażanie zmian. Jeśli już, to moje doświadczenie
wskazuje raczej na to, że w wielu przypadkach zmiany w systemach IT w
bankach potrafią trwać absurdalnie długo.

> Porozmawiajmy lepiej o programowaniu.

No to ja przecież od początku chciałem się dowiedzieć, jak to mogłoby
wyglądać od strony praktycznej, a ty mnie zbyłeś mnie opowieścią o
tablicach i flamastrach.

do góry

On Mon, 30 Mar 2015 02:15:14 -0700 (PDT), Maciej Sobczak
<s...@g...com> wrote:
> Faktycznie. Na szczęście koledzy pomogli:
>
http://www.wsj.com/articles/SB1000087239639044424690
4577572752865497064

> "a group of financial firms injecting $400 million to keep Knight
Capital G=
> roup Inc. afloat"

Skończyło się na tym, ze Knighta przejęła inna firma. Ta "pomoc" nie
była bezinteresowna.

RW

do góry

On Sat, 28 Mar 2015 13:51:39 -0500, A.L. <a...@a...com> wrote:
> Nareszcie glos rozsadku. Smaic mi sie chce ze "specjalistow"
> wypowiadajacych sie w tym watku.

Masz pogubione PL-literki i przedstawioną kolejność liter. Zakładam
jednocześnie że jesteś mistrzem w dowodzenie formalnej poprawności
itd. itp. Jak w takim razie oceniłbyś prawdopodobieństwo zaistnienia
faktu że pisząc program napiszesz np. q zamiast p? I w jaki sposób
formalny matematyczne poprawny dowód może te prawdopodobieństwo
zmienić?

Najdroższy tego rodzaju błąd kosztował, jeżeli dobrze pamiętam, grubo
ponad miliard dolarów.

Zrozum mnie dobrze: nie utrzymuję że dowody poprawności to coś
nieprzydatnego. Raczej szacuję, iż na poziomie jaki reprezentuje
większość dyskutantów na tym forum (bardziej "baza szlauchów i
kaloszy" niż awionika), nie mających takiego doświadczenia jak ty,
ważniejsze jest stosowanie elementarnych dobrych praktyk, jak np.
nieobarczanie tylko jednego programisty odpowiedzialnością za
szczególne ważny kod.

do góry

W dniu poniedziałek, 30 marca 2015 20:08:40 UTC+2 użytkownik Andrzej Jarzabek
napisał:

> Przecież nie charytatywnie, tylko żeby przejąć firmę.

Nic nie szkodzi. Ja w swoim portfelu inwestycyjnym mam podobną ilość udziałów różnych
firm inwestycyjnych właśnie po to, żeby strata Rysia i zysk Krzysia nie były
problemem, tylko co najwyżej zmianą proporcji. Zdaje się, że taka dywersyfikacja
inwestycyjna jest powszechną praktyką. Ot i cały dramat.

> Myślisz, że gdyby
> taka Toyota

Zginęli ludzie. Nie rozmawiamy o kupowaniu akcji, tylko o tworzeniu poprawnego
oprogramowania.

> A na rozbijających się samochodach Toyoty zyskuje Ford

Nie. Ford robi w gacie, bo przecież do tej pory używał dokładnie takich samych metod,
więc przypuszczalnie mają takie same problemy. Dlatego:

https://www.linkedin.com/jobs2/view/6966713

"Ford has identified the need to increase its core competency in the area of
development and verification of real-time embedded software controls using Formal
Methods."

*Has identified*. Zastanowili się nad stanem obecnym i zauważyli potrzebę. Tzn. *oni
również* zauważyli taką potrzebę.

Dokładnie o tym piszę od samego początku. O rosnącym zainteresowaniu.

Tzn. w pewnych branżach zainteresowanie rośnie a w innych nie rośnie.

> Nie zgodzę się, jak najbardziej jest presja na szukanie lepszych
> rozwiązań i wdrażanie nowych metod. Tylko że nie ma za bardzo przesłanek
> na to, że metody formalne są lepszym rozwiązaniem.

Najwyraźniej nie ma takiej potrzeby, albo się to nie kalkuluje. Od początku się w tym
temacie zgadzamy.

> moje doświadczenie
> wskazuje raczej na to, że w wielu przypadkach zmiany w systemach IT w
> bankach potrafią trwać absurdalnie długo.

Co do tego też się zgadzamy.

> > Porozmawiajmy lepiej o programowaniu.
>
> No to ja przecież od początku chciałem się dowiedzieć, jak to mogłoby
> wyglądać od strony praktycznej, a ty mnie zbyłeś mnie opowieścią o
> tablicach i flamastrach.

Nie. Napisałem wyraźnie, że zrobiłbym to dokładnie tak, jak opisałeś. Bo ja też umiem
liczyć.

Czy jest jeszcze jakiś punkt, co do którego się nie zgadzamy, czy można ten wątek
powoli domykać?

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

do góry

W dniu sobota, 28 marca 2015 10:54:16 UTC+1 użytkownik M.M. napisał:
> > >
> > > 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,
> Właśnie, tego nie da się udowodnić, a jest to też ważny aspekt
> programu. A w testach tak się robi, porównuje się kilka
> różnych algorytmów dla różnych danych.

To, że "nie istnieje w ramach określonego rozmiaru >>lepszy<< program"
jest "ważnym aspektem programu"? Dla kogo jest to ważne? Klienta
interesuje, żeby program działał zadowalająco dobrze, a nie to, żeby
"w ramach określonego rozmiaru programu nie istniał jakiś lepszy".
(W każdym razie ja nie spotkałem nigdy klienta o tak osobliwych
zainteresowaniach. Ale nawet gdybym spotkał, pewnie po prostu nie
uwierzyłbym własnym uszom)
Nie widzę też, w jaki sposób testy miałyby tu być pomocne.

> > tylko nieprecyzyjnej
> > specyfikacji. Co to znaczy,że "w ramach określonego rozmiaru program
> > jest lepszy od innego programu"?
> Zakładamy że specyfikacja jest dobra. To jest kwestia jakości
> użytych algorytmów/heurystyk.

To, co piszesz, nic nie wyjaśnia.
Powiedzenie, że coś jest najlepsze, jest po prostu powiedzeniem
nieprecyzyjnym. Co to znaczy "najlepsze"? Że przynosi najwięcej
pieniędzy? Że ma najwięcej użytkowników? Że najbardziej podoba
się klientowi?
Jeżeli podajesz jawnie złą specyfikację, to potem nie możesz mówić
"zakładamy, że specyfikacja jest dobra", bo nie jest.

> > 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),
> Nie słyszałem o logice temporalnej. Może się mylę, ale to się
> wydaje łatwe. Dla mnie taki dowód sprowadza się do tego, aby
> wszystkie pary kodu, który może wykonać się równolegle, były
> opatrzone semaforami w tej samej kolejności w sensie wykonania i
> w odwrotnej kolejności (też w sensie wykonania).

Mylisz się z pewnością, choćby dlatego, że semafor nie jest jedynym
mechanizmem synchronizującym używanym w programach wielowątkowych.

do góry