On 2011-12-22, Edek <e...@g...com> wrote:
> On 12/22/2011 01:09 AM, Andrzej Jarzabek wrote:
>> On 21/12/2011 19:37, Edek wrote:
>>>
>>> Z samego programowania dowody (pół)formalne stosuje
>>> się przy algorytmach wątkowych. Żaden unit test nie pokaże
>>> błędu wielowątkowego, co najwyżej wysypie się np. raz na 1e4.
>>
>> No więc jeśli wiesz, że błędna implementacja wysypie się raz na 1e4, to
>> jeśli zrobiłeś test, który odpala się 1e6 razy, to masz znacznie lepszą
>> gwarancję poprawności, niż gdybyś tylko zrobił dowód (pół)formalny.
>
> Bzdura...

Nie do końca. Jeśli napisałeś test *oraz* przeprowadziłeś dowód
(pół)formalny, to jesteś lepiej zabezpieczony. ale AJ pewnie chciał
zastąpić dowód testem.

--
Secunia non olet.
Stanislaw Klekot

do góry

On Dec 22, 9:19 am, "Stachu 'Dozzie' K."
<d...@g...eat.some.screws.spammer.invalid> wrote:
> On 2011-12-22, Edek <e...@g...com> wrote:
>
> >> jeśli zrobiłeś test, który odpala się 1e6 razy, to masz znacznie lepszą
> >> gwarancję poprawności, niż gdybyś tylko zrobił dowód (pół)formalny.
>
> > Bzdura...
>
> Nie do końca. Jeśli napisałeś test *oraz* przeprowadziłeś dowód
> (pół)formalny, to jesteś lepiej zabezpieczony. ale AJ pewnie chciał
> zastąpić dowód testem.

A wywnioskowałeś to z konstrukcji "lepszą [...] niż gdybyś tylko
zrobił dowód"?

do góry

W dniu 2011-12-22 09:58, Roman W pisze:

>> Jasne. Powiedzmy, że chodzi o liczby od 0 do 9 i rozkład jednostajny.
>>
>> Oto mój generator:
>>
>> int getNextValue()
>> {
>> static int x = 0;
>> if (x == 10) x = 0;
>> return x++;
>> }
>>
>> Powyższa funkcja przy odpowiednio wielu wywołaniach daje całkiem dobry
>> "histogram".
>> Można tak zrobić dowolny zadany "rozkład" i go "przetestować" tak jak
>> opisałeś.
>
> I jezeli moj generator ma sluzyc *wylacznie* do obliczania wartosci oczekiwanych
E[f(X)], gdzie X ma miec rozklad jednostajny w zbiorze {0,1,2,...,9}, to taki test w
zupelnosci wystarcza, bo korelacje pomiedzy poszczegolnymi losowaniami mnie nie
obchodza. Ba, do calkowania Monte Carlo takie generatory moga byc lepsze od
standardowych (roznica pomiedzy liczbami pseudo- i quasilosowymi).

[poznaj tejemną sztukę naciskania guzika enter]
Jakim cudem? Korelacje (ich brak) są podstawą działania MC.

Z czymś takim to dostaniesz kwadraturę N-C (o ile nie zepsujesz
i nie bedziesz np całkował po 10 wymiarowej przestrzeni tak:
F ( rand, rand...rand ) ;)

pzdr
bartekltg

do góry

On Thursday, December 22, 2011 9:40:27 AM UTC, bartekltg wrote:

> [poznaj tejemną sztukę naciskania guzika enter]
> Jakim cudem? Korelacje (ich brak) są podstawą działania MC.

Poczytaj o licbach Sobola, na przyklad.

>
> Z czymś takim to dostaniesz kwadraturę N-C (o ile nie zepsujesz
> i nie bedziesz np całkował po 10 wymiarowej przestrzeni tak:
> F ( rand, rand...rand ) ;)

Ale byla mowa o usrednianiu po rozkladzie *dyskretnym*.

RW

do góry

On 12/22/2011 10:19 AM, Stachu 'Dozzie' K. wrote:
> On 2011-12-22, Edek<e...@g...com> wrote:
>> On 12/22/2011 01:09 AM, Andrzej Jarzabek wrote:
>>> On 21/12/2011 19:37, Edek wrote:
>>>>
>>>> Z samego programowania dowody (pół)formalne stosuje
>>>> się przy algorytmach wątkowych. Żaden unit test nie pokaże
>>>> błędu wielowątkowego, co najwyżej wysypie się np. raz na 1e4.
>>>
>>> No więc jeśli wiesz, że błędna implementacja wysypie się raz na 1e4, to
>>> jeśli zrobiłeś test, który odpala się 1e6 razy, to masz znacznie lepszą
>>> gwarancję poprawności, niż gdybyś tylko zrobił dowód (pół)formalny.
>>
>> Bzdura...
>
> Nie do końca. Jeśli napisałeś test *oraz* przeprowadziłeś dowód
> (pół)formalny, to jesteś lepiej zabezpieczony. ale AJ pewnie chciał
> zastąpić dowód testem.
>

Nie. Dowód jest "pół"-formalny tylko z powodu notacji [1]. Logika
jest po prostu logiką, nie logiką humanistyczną, nie logiką
miszczów Javy, nie kobiecą, jest weryfikowalna - daje zupełną
gwarancję. Test oczywiście można zrobić, ale mam pytanie:
skąd niby ma być wiadomo, że błąd występuje raz na 1e4 i
przy jakich założeniach? Dowód formalny jest adekwatny,
a test nic nie wnosi.

Testy robi się używając do tego specjalizowanych narzędzi,
nie unit testów, tam eksponuje się częstość występowania
błędów przez uwypuklenie sekwencji czasowych wobec
prawdziwego zastosowania w kodzie, co daje o kilka rzędów
wielkości większe prawdopodobieństwo pokazania błędu,
nie czeka się miesiąc tylko kilka sekund. To nie jest
unit test, testuje się poprzez model i tylko po to,
żeby mieć szybko wynik.

Edek

[1] ... ludzie zazwyczaj w ten sposób tłumaczą, dlaczego
nie ma formy dowodu matematycznego, dlaczego używają
swojej umownej notacji, itd., żeby uniknąć zbędnych pytań
i czepiania się rzeczy tak naprawdę nieistotnych.

do góry

On Dec 22, 9:06 am, Roman W <b...@g...pl> wrote:
> On Thursday, December 22, 2011 12:09:57 AM UTC, Andrzej Jarzabek wrote:
>
> > > błędu wielowątkowego, co najwyżej wysypie się np. raz na 1e4.
>
> > No więc jeśli wiesz, że błędna implementacja wysypie się raz na 1e4, to
> > jeśli zrobiłeś test, który odpala się 1e6 razy, to masz znacznie lepszą
> > gwarancję poprawności, niż gdybyś tylko zrobił dowód (pół)formalny.
>
> A jak w produkcji algorytm wykonuje sie 24h na dobe co 10 milisekund,
> to takie dowody poprawnosci mozna sobie, hmm, wsadzic w rurke.

Nie bardzo rozumiem, chodzi o to, żeby nie przeprowadzać tego
formalnego czy półformalnego dowodu, bo można go sobie wsadzić w
rurkę? Czy żeby nie testować, bo skoro masz dowód, to testy są
niepotrzebne?

Tzn. ja bym faktycznie ostrożnie się zgodził z twierdzeniem, że w
wielu przypadkach formalne lub półformalne dowody poprawności
programów wielowątkowych mają niską wartość - jeśli synchronizacja
wątków jest na tyle skomplikowana, że taki dowód będzie nietrywialny,
to prawdopodobnie należy ją uprościć, a nie przeprowadzać dowód.
Natomiast nawet jeśli zaprojektujes algorytm i przedstawisz jego
poprawność, to znacznie trudniej będzie ci udowodnić, że program
zadany twoim kodem źródłowym faktycznie realizuje ten algorytm, a nie
- na wskutek pomyłki - trochę inny.

Natomiast w praktyce testy automatyczne potrafią wyłapać całkiem sporo
błędów - nawet takie, które działają przez kilka czy kilkanaście
minut, nie mówiąc już o tym, że po prostu możesz mieć wydzieloną
maszynę do soak testów, która mieli różne scenariusze 24/7 - to nie
jest taki gigantyczny koszt, a można to zrobić niezależnie od tego czy
i jak bardzo formalnie się dowodzi.

do góry

W dniu 2011-12-22 10:05, Roman W pisze:
> On Thursday, December 22, 2011 8:28:34 AM UTC, bartekltg wrote:
>
>> *) w pewnych przypadkach etc. Czasem nie jest to takie trywialne,
>> np. rozkład normalny generuje się dość sprytnie.
>
> Jezeli umiemy obliczyc odwrotnosc dystrybuanty, to jest latwe.

O tym ta uwaga!

A umiesz obliczyć (sprawnie i szybko) odwrotność dystrybuanty
rozkładu normalnego? Już z samą 'funkcją błędu' czyli dystrybuantę
r.normalnego musisz ładnie aproksymować.

A cały pomysł z rozkładem normalnym polega na tym, że wcale nie
musisz ograniczać się do przestrzeni jednowymairowej.
Łatwiej uzyskać rozkłąd normlany bawiąc się współrzędnymi
na płaszczyźnie. Np:

http://en.wikipedia.org/wiki/Box%E2%80%93Muller_tran
sform

Kosztem odrobiny trygonometrii i pierwiastka (albo
jednej tryg i dwóch pierwiastków:) masz dwie wylosowane
niezależne zmienne.

I wpadnięcie na to bez naprowadzenia nie jest takie łatwe.

pzdr
bartekltg

do góry

On Dec 22, 9:02 am, Roman W <b...@g...pl> wrote:
> On Thursday, December 22, 2011 12:00:11 AM UTC, Andrzej Jarzabek wrote:
> > Banalnie - zakładasz poziom pewności, np. 5 sigma i robisz skwantyzowany
> > soak test - generujesz liczby, wrzucasz w odpowiednie przedziały, jak
> > wygenerujesz odpowiednio dużo, to sprawdzasz, czy w każdym z przedziałów
> > jest odpowiednia ilość plus minus błąd. Jak ci się nie chce porządnie
> > liczyć błędów, to robisz "na oko" i ewentualnie korygujesz. Na tym
> > schemacie możesz zrobić unit test, który ci to sprawdza w pół sekundy, i
> > soak test, który leci godzinę.
>
> To sprawdza tylko rozklad, nie sprawdza czy kolejne losowania sa more or less
> niezalezne. Wystarczy do calkowania funkcji metoda Monte Carlo, nie wystarczy
> do np. symulowania procesow stochastycznych.

Na "more or less niezależność' też chyba można napisać analogiczny
test?

Oczywiście na takim poziomie ogólności nie da się odpowiedzieć, jak
testowac funkcję pseudolosową. Najpierw należałoby ustalić, do czego
jest ta funkcja potrzebna i jakie właściwości ma w związku z tym mieć,
czy jest to własny algorytm, własna implementacja opublikowanego
algorytmu, o którym wiemy, że ma takie właściwości, czy po prostu
wrapper na istniejącą wcześniej implementację, której jakość chcemy/
musimy zweryfikować.

do góry

W dniu 2011-12-22 10:44, Roman W pisze:
> On Thursday, December 22, 2011 9:40:27 AM UTC, bartekltg wrote:
>
>> [poznaj tejemną sztukę naciskania guzika enter]
>> Jakim cudem? Korelacje (ich brak) są podstawą działania MC.
>
> Poczytaj o licbach Sobola, na przyklad.


I jak ma się to do przykładu 1,2,3,4.
I nadal podtrzymuje zdanie, że to zwykła
kwadratura, nie MC (MC nie kończą się na CMC)

>> Z czymś takim to dostaniesz kwadraturę N-C (o ile nie zepsujesz
>> i nie bedziesz np całkował po 10 wymiarowej przestrzeni tak:
>> F ( rand, rand...rand ) ;)
>
> Ale byla mowa o usrednianiu po rozkladzie *dyskretnym*.

Spojrz raz jeszcze na tamtą implementację, na funkcję
zdefiniowaną na dyskretnej kostce {1..10}^10

>> F ( rand, rand...rand ) ;)
(10 razy wołany rand)

Teraz jesne:>

No, chyba, ze dla Ciebie zbiór dyskretny to tylko 1..n.
Można sobie przenumerować, ale jeśli używamy MC to znaczy,
że nie możemy zrobić n odpaleń funkcji, bo czasu nie starczy.

pzdr
bartekltg

do góry

On Thursday, December 22, 2011 10:07:32 AM UTC, bartekltg wrote:
> W dniu 2011-12-22 10:44, Roman W pisze:
> > On Thursday, December 22, 2011 9:40:27 AM UTC, bartekltg wrote:
> >
> >> [poznaj tejemną sztukę naciskania guzika enter]
> >> Jakim cudem? Korelacje (ich brak) są podstawą działania MC.
> >
> > Poczytaj o licbach Sobola, na przyklad.
>
>
> I jak ma się to do przykładu 1,2,3,4.

Ale kto wlasciwie mowi, ze generator 1,2,3,4 jest dobry? Nie jest. Caly moj argument
to to, ze jezeli uzywam generatora do calkowania MC, to wystarczy sprawdzac
histogram. Jesli calkuje w N wymiarach, to histogram musi byc N-wymiarowy, to
oczywiscie bardzo utrudnia testowanie, ale ludzie takie testy robili (np. w ksiazce
Jaeckla).

RW

do góry