-
Data: 2015-03-31 14:48:32
Temat: Re: poprawność algorytmu
Od: "M.M." <m...@g...com> szukaj wiadomości tego autora
[ pokaż wszystkie nagłówki ]On Tuesday, March 31, 2015 at 12:20:29 PM UTC+2, g...@g...com wrote:
> 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?
Uprościłem pewien aspekt złożoności do 'rozmiaru' - miałem bardzo
podobną sytuację w praktyce. Ale ok, nie ciągnijmy.
> Klienta interesuje, żeby program działał zadowalająco dobrze, a nie to, żeby
> "w ramach określonego rozmiaru programu nie istniał jakiś lepszy".
Nie zgodzę się, klient może chcieć aby program działał jak najlepiej
to możliwe - w ramach jakiś ograniczeń.
> (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)
Dlaczego byś nie uwierzył? Program wspomaga decyzje. Od decyzji zależy
(w jakimś stopniu) generowanie zysków. Co w tym dziwnego, że chcemy
aby taki program działał jak najlepiej.
Inny przykład, program do translacji języków naturalnych. Dlaczego
chciałbyś używać gorszy program niż lepszy?
Następny problem: gra w szachy. Dlaczego używać słabszego programu niż
silniejszego? Można mnożyć...
> Nie widzę też, w jaki sposób testy miałyby tu być pomocne.
Bierzesz wiele danych wejściowych, porównujesz jakość odpowiedzi i
oceniasz. A jak na podstawie kodu udowodnić, że jeden program lepiej
translatuje, albo lepiej gra w szachy, od drugiego?
>
> > > 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.
Wiadomo że jest nieprecyzyjnym. W każdym przypadku co innego
oznacza najlepszy. W każdym przypadku chodzi o inną jakość algorytmów czy
heurystyk. Obojętnie o jaką jakość chodzi, to trudno dowieść jej
formalnie na podstawie kodu.
> Co to znaczy "najlepsze"? Że przynosi najwięcej
> pieniędzy? Że ma najwięcej użytkowników? Że najbardziej podoba
> się klientowi?
Tak, dobre przykłady.
> Jeżeli podajesz jawnie złą specyfikację, to potem nie możesz mówić
> "zakładamy, że specyfikacja jest dobra", bo nie jest.
Można tak mówić, ponieważ to generalne określenie w każdym przypadku
się konkretyzuje. Bez względu na to jak się skonkretyzuje, to ciężko
dokonać takiego dowodu formalnego.
>
> > > 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.
Jeśli odebrałeś moje słowa dosłownie, to mam prośbę. Najpierw uogólnij
sobie mój 'semafor' na inne mechanizmy synchronizowania, a potem
przeanalizuj czy się mylę. Potem pogadamy dalej.
Następne wpisy z tego wątku
- 31.03.15 16:39 g...@g...com
- 31.03.15 19:08 slawek
- 31.03.15 19:29 M.M.
- 31.03.15 19:43 M.M.
- 31.03.15 19:49 g...@g...com
- 31.03.15 19:59 slawek
- 31.03.15 20:10 slawek
- 31.03.15 20:34 g...@g...com
- 31.03.15 21:01 M.M.
- 31.03.15 23:04 slawek
- 31.03.15 23:25 g...@g...com
- 31.03.15 23:32 Andrzej Jarzabek
- 31.03.15 23:59 slawek
- 01.04.15 00:08 g...@g...com
- 01.04.15 08:46 firr
Najnowsze wątki z tej grupy
- Nauka i Praca Programisty C++ w III Rzeczy (pospolitej)
- testy-wyd-sort - Podsumowanie
- Tworzenie Programów Nieuprzywilejowanych Opartych Na Wtyczkach
- Do czego nadaje się QDockWidget z bibl. Qt?
- Bibl. Qt jest sztucznie ograniczona - jest nieprzydatna do celów komercyjnych
- Co sciaga kretynow
- AEiC 2024 - Ada-Europe conference - Deadlines Approaching
- Jakie są dobre zasady programowania programów opartych na wtyczkach?
- sprawdzanie słów kluczowych dot. zła
- Re: W czym sie teraz pisze programy??
- Re: (PDF) Surgical Pathology of Non-neoplastic Gastrointestinal Diseases by Lizhi Zhang
- CfC 28th Ada-Europe Int. Conf. Reliable Software Technologies
- Młodzi programiści i tajna policja
- Ada 2022 Language Reference Manual to be Published by Springer
- Press Release - AEiC 2023, Ada-Europe Reliable Softw. Technol.
Najnowsze wątki
- 2024-09-02 Wzór
- 2024-09-01 Polska-Chorwacja 650zł elektrykiem
- 2024-09-01 odrdzewiacz do amelinium
- 2024-09-01 Elektryczna łapka i szerszeń
- 2024-09-01 Jakie podatki za wynajem?
- 2024-09-02 Warszawa => Key Account Manager <=
- 2024-09-02 Warszawa => Projektant/Programista React Native <=
- 2024-09-02 Gdańsk => Head of International Freight Forwarding Department <=
- 2024-09-02 Warszawa => Sales Development Representative (in German) <=
- 2024-09-01 1. wrzesnia po niemiecku
- 2024-09-01 Od setki do setki...
- 2024-08-31 wpadłem w siodło
- 2024-08-25 cenka opada
- 2024-08-30 Elektryki takie bezpieczne cd.
- 2024-08-31 Warszawa => International freight forwarder <=