-
Data: 2015-03-27 11:09:18
Temat: Re: poprawność algorytmu
Od: g...@g...com szukaj wiadomości tego autora
[ pokaż wszystkie nagłówki ]W dniu piątek, 27 marca 2015 10:06:11 UTC+1 użytkownik Maciej Sobczak napisał:
>
> > No to teraz całkowicie bez szydery i na poważnie spytam, jakie są
> > praktyczne możliwości. Mam powiedzmy program w C++, kilkaset tysięcy
> > linii kodu, korzysta z boosta, wątków, libc, bazy danych, MOM-a itd. -
> > co można zrobić żeby udowodnuć jego poprawność i ile to będzie kosztowało?
>
> Nie da się. Dla równowagi zauważmy jednak, że przetestować
> tego też się nie da, zresztą dokładnie z tych samych powodów
> (uwaga logiczna: z tezy że się nie da konsekwentnie wynika
> też teza, że się tego nie robi; można co najwyżej udawać że
> się robi pomijając milcząco tą drobną niedogodność, że się
> nie da i tak właśnie działa większa część branży, patrz też niżej).
Tutaj akurat widzę pomylenie pojęć. Testowanie to uruchamianie
programu z założeniem sprawdzenia, jak się zachowuje w określonych
okolicznościach. Nie wiem, dlaczego programów napisanych w C++
miałoby się nie dać uruchomić z zamiarem sprawdzenia, jak się zachowuje
w określonych okolicznościach.
> Na poważnie - nie stosuje się metod formalnych a posteriori
> w odniesieniu do kodu, który nie był pisany z myślą o takich
> metodach. Problem stopu, Goedel, i podobne teoretyczne przeszkody.
> Natomiast da się napisać (i to udowodnić) poprawny program,
> jeśli się go pisze z myślą o takich metodach.
> Co ciekawe, dotyczy to również testów i to z takich samych powodów.
To jest ciekawe pytanie: jakie znacie systemy stworzone z myślą
o dowodzeniu poprawności napisanych w nich programów?
I przy okazji kilka ciekawostek, które ostatnio przebiegły twittera:
"What if you could write a test for a problem and have your compiler automatically
return a correct implementation?":
http://blogs.teamb.com/craigstuntz/2014/07/07/38818/
Microsoft (chyba wczoraj) wypuścił źródła systemu Z3 używanego w w/w
artykule: github.com/Z3Prover/z3
Dowód sprzeczności w systemie Coq: https://github.com/clarus/falso
> Ćwiczenie logiczne: jeżeli ktoś twierdzi, że testuje swój program,
> to ja poproszę o *dowód*, że testowanie jest kompletne.
Na tym chyba polega istotowa różnica między dowodem a testowaniem,
że dowód wyczerpuje wszystkie możliwości, a testowanie nie.
"Kompletne testowanie" byłoby właśnie -- po prostu -- dowodem.
Następne wpisy z tego wątku
- 27.03.15 12:24 M.M.
- 27.03.15 13:21 g...@g...com
- 27.03.15 15:12 Maciej Sobczak
- 27.03.15 16:00 g...@g...com
- 27.03.15 21:25 Andrzej Jarzabek
- 28.03.15 05:04 M.M.
- 28.03.15 09:40 Maciej Sobczak
- 28.03.15 09:45 g...@g...com
- 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
Najnowsze wątki z tej grupy
- 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.
- Ada-Europe - AEiC 2023 early registration deadline approaching
- Ada-Europe Int.Conf. Reliable Software Technologies, AEiC 2023
- Ile cykli zajmuje mnożenie liczb 64-bitowych?
Najnowsze wątki
- 2024-07-02 Realme 7 Na co zmienić?
- 2024-06-27 Prywatny parking? Pierwsze 10 minut bezplatnie
- 2024-07-02 znalazłem samochód ;)
- 2024-07-02 Pierwszeństwo łamane
- 2024-07-02 zamek
- 2024-07-02 Akumulatory VRLA
- 2024-07-03 Białystok => Inżynier DevOps Conexa First (Kontraktor) <=
- 2024-07-03 MĂźnchen => Test Development Engineer (m/w/d) <=
- 2024-07-03 Warszawa => Full Stack web developer (obszar .Net Core, Angular6+) <=
- 2024-07-03 Warszawa => Programista Full Stack (.Net Core) <=
- 2024-07-02 Kraków => Spedytor międzynarodowy <=
- 2024-07-02 Poznań => Senior React Native Developer <=
- 2024-07-02 Rzeszów => Frontend Developer (React) <=
- 2024-07-02 Warszawa => Fullastack (Java) Developer <=
- 2024-07-02 reparacje