On Dec 22, 8:47 am, Edek <e...@g...com> wrote:
> On 12/22/2011 01:09 AM, Andrzej Jarzabek wrote:
>
> > 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...

Bzdura, że bzdura.

do góry

On Thursday, December 22, 2011 10:02:17 AM UTC, bartekltg wrote:
> 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?

http://home.online.no/~pjacklam/notes/invnorm/

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

Po to sa ksiazki. Natomiast metoda Box-Muller wcale nie jest taka dobra. "Ziggurat"
jest lepszy.

RW

do góry

On Thursday, December 22, 2011 9:55:37 AM UTC, Andrzej Jarzabek wrote:

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

Problem polega na tym, ze dowolny test robisz dla danych, ktore znasz. Natomiast
jezeli masz logiczny dowod, ze implementacja jest poprawna i algorytm jest poprawny,
to wiesz ze zadziala dla dowolnych danych akceptowanych przez algorytm.

RW

do góry

On 12/22/2011 10:29 AM, Andrzej Jarzabek wrote:
> 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"?

Ok, podzielę włos na czworo. Mamy P1() = 1, i P2() = x.
Ile wynosi prawdopodobieństwo P1 | P2, i czy w ogóle zależy od P2?

Idać dalej proponowaną logiką "lepszości", myślę, że faktycznie
test zastąpiłby napisanie poprawnego algorytmu.

Edek

do góry

On 2011-12-22, Edek <e...@g...com> wrote:
> 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].

Nie zrozumiałeś. Nacisk jest na spójnik "oraz". Dowód i test razem
wzięte zabezpieczają lepiej (a na pewno nie gorzej) niż sam dowód albo
niż sam test.

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

Jeśli test nie przechodzi, to sygnał, że trzeba się czemuś przyjrzeć.
I to prawdopodobnie kodowi, który się zmieniał (więc raczej nie kodowi
testu). Nie mówię że test zastępuje dowód. Test może dowodowi *pomóc*.

--
Secunia non olet.
Stanislaw Klekot

do góry

On 12/22/2011 11:15 AM, Andrzej Jarzabek wrote:
> On Dec 22, 8:47 am, Edek<e...@g...com> wrote:
>> On 12/22/2011 01:09 AM, Andrzej Jarzabek wrote:
>>
>>> 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...
>
> Bzdura, że bzdura.

Heh, powiedz dlaczego...

do góry

W dniu 2011-12-22 11:17, Roman W pisze:
> On Thursday, December 22, 2011 10:02:17 AM UTC, bartekltg wrote:
>> 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?
>
> http://home.online.no/~pjacklam/notes/invnorm/

Dać się da. Ale kosztowne

>
>> 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.
>
> Po to sa ksiazki.

To dlaczego dyskutujesz ze stwierdzeniem, że poza sztuczką
z odwrotną dystrybuantą istnieją bardziej wyrafinowane
i mniej trywialne pomysły.

> Natomiast metoda Box-Muller wcale nie jest taka dobra.

Co jej dolega?

> "Ziggurat" jest lepszy.

Niby ciut szybszy (ale raczej w dłuższych seriach), ale
bardziej skomplikowany. Tylko o szybkość chodzi?

pzdr
bartekltg

do góry

W dniu 2011-12-22 11:14, Roman W pisze:
> 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).

ENTER naciskaj!

Cały czas utożsamiasz MC z CMC czyli podstawieniem
sumowania f(rand). Taki Metropolis już na tym może nie
pojechać (odpowiednio sprawnie). Ciężko więc pisać
ogólnie o całkowaniu MC.

pzdr
bartekltg

do góry

On Dec 22, 10:34 am, Edek <e...@g...com> wrote:
> On 12/22/2011 10:29 AM, Andrzej Jarzabek wrote:
>
> > 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"?
>
> Ok, podzielę włos na czworo. Mamy P1() = 1, i P2() = x.
> Ile wynosi prawdopodobieństwo P1 | P2, i czy w ogóle zależy od P2?

A co twoje P1 i P2 mają wspólnego z opisywaną sytuacją?

> Idać dalej proponowaną logiką "lepszości", myślę, że faktycznie
> test zastąpiłby napisanie poprawnego algorytmu.

Myślę, że to tylko świadczy o możliwościach kolegi w kwestii pójścia
gdziekolwiek z logiką.

do góry

W dniu 2011-12-22 11:28, Roman W pisze:
> On Thursday, December 22, 2011 9:55:37 AM UTC, Andrzej Jarzabek wrote:
>
>> 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.
>
> Problem polega na tym, ze dowolny test robisz dla danych, ktore znasz. Natomiast
jezeli masz logiczny dowod, ze implementacja jest poprawna i algorytm jest poprawny,
to wiesz ze zadziala dla dowolnych danych akceptowanych przez algorytm.

Nie zawsze. Losowane dane (losowy przegląd przestrzeni danych) może
coś istotnego wykryć.

Oczywiście dowód poprawności algorytmu jest lepszy. Do tego trzeba
jeszcze dodać dowód poprawności implementacji. Co w sumie jest zazwyczaj
drogie. Testy mają szansę złapać błąd zanim znajdziesz go w trakcie
przeprowadzania dowodu. Co oczywiście nie znaczy, że "przetestowane"
oznacza "poprawne". Oznacza tylko "większa szansa, że jest poprawne".

Decyzja, co robić (dowód, testy na dużej ilości danych), jest już
decyzją biznesową.

--
Paweł Kierski
n...@p...net

do góry