-
Data: 2015-03-28 09:45:21
Temat: Re: poprawność algorytmu
Od: g...@g...com szukaj wiadomości tego autora
[ pokaż wszystkie nagłówki ]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.
Następne wpisy z tego wątku
- 28.03.15 10:10 Maciej Sobczak
- 28.03.15 10:47 g...@g...com
- 28.03.15 10:54 M.M.
- 28.03.15 11:46 M.M.
- 28.03.15 11:54 Andrzej Jarzabek
- 28.03.15 13:08 Andrzej Jarzabek
- 28.03.15 18:22 Maciej Sobczak
- 28.03.15 19:38 Roman W
- 28.03.15 19:43 Roman W
- 28.03.15 19:50 A.L.
- 28.03.15 19:51 A.L.
- 28.03.15 21:16 Andrzej Jarzabek
- 29.03.15 00:13 Maciej Sobczak
- 29.03.15 15:21 Andrzej Jarzabek
- 29.03.15 23:18 Maciej Sobczak
Najnowsze wątki z tej grupy
- Popr. 14. Nauka i Praca Programisty C++ w III Rzeczy (pospolitej)
- Arch. Prog. Nieuprzywilejowanych w pełnej wer. na nowej s. WWW energokod.pl
- 7. Raport Totaliztyczny: Sprawa Qt Group wer. 424
- TCL - problem z escape ostatniego \ w nawiasach {}
- 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
Najnowsze wątki
- 2025-01-20 Gdańsk => Programista Full Stack .Net <=
- 2025-01-20 Gliwice => Business Development Manager - Dział Sieci i Bezpieczeńst
- 2025-01-20 Warszawa => Full Stack .Net Engineer <=
- 2025-01-20 huta ruszyla
- 2025-01-20 piece wodorowe
- 2025-01-20 Lublin => Programista Delphi <=
- 2025-01-20 Warszawa => Architekt rozwiązań (doświadczenie w obszarze Java, AWS
- 2025-01-20 Mińsk Mazowiecki => Area Sales Manager OZE <=
- 2025-01-20 Bieruń => Spedytor Międzynarodowy (handel ładunkami/prowadzenie flo
- 2025-01-19 Test - nie czytać
- 2025-01-19 qqqq
- 2025-01-19 Tauron przysyła aneks
- 2025-01-19 Nowa ładowarka Moya a Twizy -)
- 2025-01-18 Power BANK z ładowaniem przelotowym robi PRZERWY
- 2025-01-18 Pomoc dla Filipa ;)