-
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
- Alg. kompresji LZW
- 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??
Najnowsze wątki
- 2025-02-27 potwierdzenie notarialne dokumentow tozsamosci ze zdjeciem
- 2025-02-27 Warszawa => Account Manager - Sprzedaż Usług Rekrutacyjnych <=
- 2025-02-27 Katowice => Regionalny Kierownik Sprzedaży (OZE) <=
- 2025-02-27 Warszawa => Mid IT Recruiter <=
- 2025-02-27 Warszawa => Expert Recruiter 360 <=
- 2025-02-27 Warszawa => Junior Rekruter <=
- 2025-02-27 China-Kraków => Key Account Manager IT <=
- 2025-02-27 Warszawa => Sales Assistant <=
- 2025-02-27 Kraków => Frontend Vue Developer <=
- 2025-02-27 Re: Zwolniony z IKEA za "wąty" przeciw firmowej promocji LGBT-IQ+ przywrócony do pracy - SN odrzucił kasacje (sygn. akt I PSK 62/24)
- 2025-02-27 Częstochowa => Manager ds. produktu <=
- 2025-02-27 Warszawa => Business Systems Analyst <=
- 2025-02-27 Nagranie poglądowe
- 2025-02-26 Zasilacz USB na ścianę.
- 2025-02-26 Błonie => Specjalista ds. public relations <=