-
Data: 2015-03-26 22:29:57
Temat: Re: poprawność algorytmu
Od: Andrzej Jarzabek <a...@g...com> szukaj wiadomości tego autora
[ pokaż wszystkie nagłówki ]On 26/03/2015 15:03, Maciej Sobczak wrote:
>
>> Nie znam się na algorytmach i ich dowodzeniu, ale mogę powiedzieć
>> tyle, że normalną praktyką w przemyśle jest testowanie a nie
>> dowodzenie,
>
> Głównie dlatego, że testowanie jest zrozumiałe zarówno dla tych,
> którzy to robią, jak i dla tych, którzy to mają zaakceptować jako
> element projektu (czytaj: zapłacić za to lub uznać jego ważność). W
> przeciwieństwie do dowodów, które są niezrozumiałe i stąd też
> niechętnie akceptowane.
No więc pomijając płacenie itd., to jest bardzo istotne kryterium, bo
jeśli formalny zapis nawet nie tylko samego dowodu, ale również
kryterium poprawności, które zostało dowiedzione, jest niezrozumiałe dla
osób, które rozmieją, kiedy program jest rzeczywiście poprawny, to cały
dowód poprawności jest OKDR.
>> bo dowodzenie jest bardzo kosztowne - jest uważane za nieopłacalne
>
> Nie. Zainteresowanie dowodzeniem rośnie właśnie dlatego, że jest
> tańsze. Może być nawet dużo tańsze.
Stąd gdzie ja stoję, tego zainteresowania nie widać.
>> nawet tam, gdzie wchodzą w grę wielomilionowe straty (np. w
>> finansach),
>
> W finansach nie ma strat. Albo się "traci" coś, czego nigdy nie było
> (wtedy nie ma strat), albo można to stosunkowo łatwo odkręcić przez
> reklamacje i wtedy (relatywnie) też nie ma strat.
>
> Masz rację, że w finansach nie stosuje się dowodów ale nie dlatego,
> że są droższe od testów, tylko dlatego, że testów też się tam nie
> robi.
Nie wątpię, że nieskończenie lepiej ode mnie znasz się na metodach
formalnych, ale w tej kwestii nie masz pojęcia o czym mówisz.
>> a zaczyna się je stosować AFAIK gdzieś w okolicach oprogramowania
>> pojazdów kosmicznych - duże potencjalne straty, stosunkowo mała
>> liczba linii kodu.
>
> Dowody da się automatyzować. Przy dużej liczbie linii kodu nie masz
> szans go pokryć testami, natomiast nadal masz szansę robić dowody.
> Stąd też to rosnące zainteresowanie.
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?
Następne wpisy z tego wątku
- 27.03.15 09:13 M.M.
- 27.03.15 10:06 Maciej Sobczak
- 27.03.15 10:57 g...@g...com
- 27.03.15 11:09 g...@g...com
- 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.
Najnowsze wątki z tej grupy
- Grok zaczął nadużywać wulgaryzmów i wprost obrażać niektóre znane osoby
- Can you activate BMW 48V 10Ah Li-Ion battery, connecting to CAN-USB laptop interface ?
- We Wrocławiu ruszyła Odra 5, pierwszy w Polsce komputer kwantowy z nadprzewodzącymi kubitami
- Ada-Europe - AEiC 2025 early registration deadline imminent
- John Carmack twierdzi, że gdyby gry były optymalizowane, to wystarczyły by stare kompy
- Ada-Europe Int.Conf. Reliable Software Technologies, AEiC 2025
- Linuks od wer. 6.15 przestanie wspierać procesory 486 i będzie wymagać min. Pentium
- ,,Polski przemysł jest w stanie agonalnym" - podkreślił dobitnie, wskazując na brak zamówień.
- Rewolucja w debugowaniu!!! SI analizuje zrzuty pamięci systemu M$ Windows!!!
- Brednie w wiki - hasło Dehomag
- Perfidne ataki krakerów z KRLD na skrypciarzy JS i Pajton
- Instytut IDEAS może zacząć działać: "Ma to być unikalny w europejskiej skali ośrodek badań nad sztuczną inteligencją."
- Instytut IDEAS może zacząć działać: "Ma to być unikalny w europejskiej skali ośrodek badań nad sztuczną inteligencją."
- Instytut IDEAS może zacząć działać: "Ma to być unikalny w europejskiej skali ośrodek badań nad sztuczną inteligencją."
- U nas propagują modę na SI, a w Chinach naukowcy SI po kolei umierają w wieku 40-50lat
Najnowsze wątki
- 2025-07-25 Drastycznie rośnie import stali - w hucie w Dąbrowie Górniczej zostanie wygaszony wielki piec
- 2025-07-25 Drastycznie rośnie import stali - w hucie w Dąbrowie Górniczej zostanie wygaszony wielki piec
- 2025-07-25 I kolejny inżynier...
- 2025-07-25 Kobiety, bójcie się inżynierów...
- 2025-07-25 Warszawa => Konsultant Wiodący SAP PP <=
- 2025-07-25 Re: Brawo !!! Osy chronione w Niemczech. Za usunięcie gniazda grozi mandat
- 2025-07-25 cudzoziemiec bez biletu
- 2025-07-25 Gdynia => Sales Executive / KAM <=
- 2025-07-25 Inżynierzy z prawomocnym...
- 2025-07-25 Łódź => Mainframe (z/OS, Assembler) Developer <=
- 2025-07-25 Warszawa => Inżynier oprogramowania .Net <=
- 2025-07-25 Kraków => Senior Fullstack Engineer (Low-Code Platform) <=
- 2025-07-25 Skrobanie
- 2025-07-25 Lublin => Konsultant ds. Wdrożeń ERP (moduł FK) <=
- 2025-07-25 Warszawa => Senior Frontend Developer (React + React Native) <=