Czy dowody poprawności kodu kiedykolwiek znajdą się w głównym nurcie? [Zamknięte]

14

Wszystkie z wyjątkiem najbardziej trywialnych programów są pełne błędów, więc wszystko, co obiecuje ich usunięcie, jest wyjątkowo pociągające. W chwili obecnej dowody poprawności są niezwykle ezoteryczne, głównie ze względu na trudność w nauce tego i dodatkowy wysiłek, jaki należy podjąć, aby udowodnić poprawność programu. Czy myślisz, że sprawdzanie kodu kiedykolwiek wystartuje?

programming-practices Casebash
źródło

Odpowiedzi:

8

Nie do końca w tym sensie, ale czyste funkcjonalne programowanie jest dobre w tej dziedzinie. Jeśli używasz Haskell, prawdopodobnie Twój program jest poprawny, jeśli kod się skompiluje. Z wyjątkiem IO dobry system typów jest dobrą pomocą.

Pomocne może być również programowanie do umowy. Zobacz umowy Microsoft Code

Jonas
źródło
6
Przepraszam - nie zrobiłem dużo „prawdziwego świata” Haskell, ale wykonałem wystarczająco dużo ćwiczeń samouczka przez kilka wcieleń. To, że się kompiluje, nie oznacza, że ​​prawdopodobnie będzie działać. W porównaniu z np. Adą (wybraną, ponieważ jest to język imperatywny o ściśle statycznym typie), powiedziałbym, że Haskell jest nieco łatwiejszy, ale głównie dlatego, że jest bardziej zwięzły (mniejsza złożoność cykliczna). Gdy mamy do czynienia z IO monady, są kłopoty, które mogą sprawić Haskell bardziej trudne, aby uzyskać prawo - to jest po prostu inny dostatecznie od bezwzględnej stylu, że są rzeczy nie można robić, co w sposób naturalny.
Steve314,
Przy opcji „nie można robić tak naturalnie”, należy rozważyć pętlę „while”. Tak, możesz rzucić własnym - ale warunek while musi znajdować się w monadzie, ponieważ musi reagować na skutki uboczne ciała pętli. Nie tylko oznacza to, że masz pozwolenie na wywoływanie efektów ubocznych w warunku while, ale także sprawia, że ​​korzystanie z tej pętli podczas jest niewygodne. Wynik końcowy - generalnie łatwiej jest używać rekurencji nawet w kodzie monad IO - a to oznacza, że ​​musisz ustrukturyzować rzeczy w określony sposób.
Steve314,
14

Wszystkie oprócz najbardziej trywialnych programów

nie można w pełni udowodnić, że jest poprawny przy rozsądnym wysiłku. Do każdego formalnego dowodu poprawności potrzebujesz co najmniej formalnej specyfikacji, która musi być kompletna i poprawna. Zazwyczaj nie jest to nic, co można łatwo stworzyć dla większości programów w świecie rzeczywistym. Na przykład spróbuj napisać taką specyfikację dla czegoś takiego jak interfejs użytkownika tej witryny dyskusji, a wiesz, co mam na myśli.

Tutaj znalazłem fajny artykuł na ten temat:

http://www.encyclopedia.com/doc/1O11-programcorrectnessproof.html

Doktor Brown
źródło
Zgadza się - w przypadku każdego projektu programistycznego następuje przejście od nieformalnego opisu problemu do formalnego (zwykle dzisiaj w formie programu) i to nie zniknie.
David Thornley,
astree.ens.fr Zobacz tutaj zastosowania przemysłowe Astrée
zw324,
@ZiyaoWei: takie narzędzia są pomocne, ale znajdują tylko niektóre błędy formalne, a nie więcej. Jeżeli taki program jednowierszowy printf("1")jest poprawny lub nie (na przykład, ponieważ wymaganiem było „wydrukować równomiernie rozłożoną liczbę losową od 1 do 6”), taki statyczny analizator nie może zdecydować.
Doc Brown
10

Problem z formalnymi dowodami polega na tym, że przesuwa problem tylko o krok wstecz.

Powiedzenie, że program jest poprawny, jest równoznaczne z powiedzeniem, że program robi to, co powinien. Jak zdefiniujesz, co powinien zrobić program? Ty to określasz. Jak zdefiniujesz, co program powinien zrobić w przypadkach, których specyfikacja nie obejmuje? Cóż, więc musisz sprecyzować specyfikację.

Powiedzmy, że twoja specyfikacja w końcu staje się wystarczająco szczegółowa, aby opisać prawidłowe zachowanie każdego aspektu całego programu. Teraz potrzebujesz sposobu, aby twoje narzędzia sprawdzające to zrozumiały. Musisz przetłumaczyć specyfikację na język formalny, który zrozumie narzędzie sprawdzania ... hej, poczekaj chwilę!

Mason Wheeler
źródło
2
Ponadto .. „Uwaga na błędy w powyższym kodzie; udowodniłem tylko, że jest poprawny, a nie wypróbowałem”. - Donald Knuth
Brendan
8

Formalna weryfikacja przeszła długą drogę, ale zwykle w branży / szeroko stosowane narzędzia pozostają w tyle za najnowszymi badaniami. Oto niektóre ostatnie wysiłki w tym kierunku:

Spec # http://research.microsoft.com/en-us/projects/specsharp/ To jest rozszerzenie C #, które obsługuje kontrakty kodowe (warunki przed / po i niezmienniki) i może wykorzystywać te kontrakty do przeprowadzania różnego rodzaju analiz statycznych .

Podobne projekty istnieją dla innych języków, takich jak JML dla java, a Eiffel ma to dość wbudowane.

Idąc dalej, projekty takie jak slam i blast mogą być używane do weryfikacji pewnych właściwości behawioralnych przy minimalnej adnotacji / interwencji programisty, ale nadal nie mogą poradzić sobie z pełną ogólnością współczesnych języków (rzeczy takie jak przepełnienie liczb całkowitych / arytmetyka wskaźnika nie są modelowane).

Wierzę, że w przyszłości zobaczymy znacznie więcej tych technik stosowanych w praktyce. Główną barierą jest to, że niezmienniki programu są trudne do wnioskowania bez ręcznych adnotacji, a programiści zwykle nie chcą dostarczać tych adnotacji, ponieważ jest to zbyt żmudne / czasochłonne.

Lucina
źródło
4

Nie, chyba że pojawi się metoda automatycznego udowodnienia kodu bez obszernej pracy programisty.

Fishtoaster
źródło
Zastanów się nad argumentem ekonomicznym: być może programiści powinni „marnować” czas na sprawdzanie poprawności, niż tracić pieniądze z powodu błędów oprogramowania.
Andres F.,
Zgadzam się z Fishtoasterem, chyba że dużo mniej zasobów wymaga dużej ilości zwykłego oprogramowania biznesowego, ale po prostu nie będzie miał kosztów / korzyści do obsługi tego poziomu poprawności. W aplikacji LOB dla uwięzionych odbiorców czasem największą korzyścią biznesową związaną z kosztami związanymi z raportem o błędzie jest dodanie do dokumentów wiersza z informacją „nie rób tego”
Bill
3

Niektóre narzędzia metod formalnych (np. Frama-C do krytycznego oprogramowania wbudowanego C) mogą być postrzegane jako (rodzaj) dostarczania lub przynajmniej sprawdzania (poprawności) dowodu danego oprogramowania. (Frama-C sprawdza, czy program przestrzega sformalizowanej specyfikacji w pewnym sensie i przestrzega wyraźnie niezmienników w programie).

W niektórych sektorach możliwe są takie formalne metody, np. DO-178C dla krytycznego oprogramowania w cywilnych statkach powietrznych. W niektórych przypadkach takie podejścia są możliwe i pomocne.

Oczywiście opracowanie mniej wadliwego oprogramowania jest bardzo kosztowne. Ale podejście formalne ma sens w przypadku pewnego rodzaju oprogramowania. Jeśli jesteś pesymistą, możesz pomyśleć, że błąd został przeniesiony z kodu do jego formalnej specyfikacji (która może zawierać pewne „błędy”, ponieważ sformalizowanie zamierzonego zachowania oprogramowania jest trudne i podatne na błędy).

Basile Starynkevitch
źródło
3

Natknąłem się na to pytanie i myślę, że ten link może być interesujący:

Zastosowania przemysłowe Astrée

Udowodnienie braku RTE w systemie używanym przez Airbusa z ponad 130 tys. Linii kodu w 2003 roku nie wydaje się złe i zastanawiam się, czy ktoś będzie mówić, że to nie jest prawdziwy świat.

zw324
źródło
2

Nie. Powszechnym przysłowiem tego jest: „W teorii teoria i praktyka są takie same. W praktyce nie”.

Jeden bardzo prosty przykład: literówki.

Właściwie uruchomienie kodu przez testowanie jednostkowe niemal natychmiast wykrywa takie rzeczy, a spójny zestaw testów neguje potrzebę jakichkolwiek formalnych dowodów. Wszystkie przypadki użycia - dobre, złe, błędy i zbocza - powinny być wyliczone w testach jednostkowych, które kończą się jako lepszy dowód, że kod jest poprawny niż jakikolwiek inny dowód niezależny od kodu.

Zwłaszcza jeśli wymagania ulegną zmianie lub algorytm zostanie zaktualizowany w celu naprawienia błędu - formalny dowód prawdopodobnie skończy się nieaktualny, tak jak to często bywa z komentarzami do kodu.

Izkata
źródło
3
Źle. Żadne testy jednostkowe nigdy nie będą w stanie objąć całego zakresu możliwych parametrów. Wyobraź sobie „testowanie jednostkowe” kompilatora w ten sposób, upewniając się, że semantyka nie zmienia wyniku.
SK-logic,
3
testowanie jednostkowe nie jest świętym Graalem ...
Ryathal
1
@Winston Ewert, istnieją sprawdzone kompilatory (i wiele innych zweryfikowanych asemblerów). A sprzęt jest formalnie weryfikowany znacznie częściej niż oprogramowanie. Zobacz tutaj: gallium.inria.fr/~xleroy/publi/compiler-certif.pdf
SK-logic
1
@ SK-logic, tak, istnieją kompilatory zabawek sprawdzone pod kątem akademickim. Ale co z kompilatorami, których ludzie faktycznie używają? Podejrzewam, że większość kompilatorów jest sprawdzana przy użyciu różnych form zautomatyzowanych testów i prawie nie dokonuje się żadnych formalnych poprawnych dowodów.
Winston Ewert
1
@Winston Ewert, dowody poprawności są praktyczne i szeroko stosowane w prawdziwym życiu. To, co nie jest bardzo praktyczne, to większość współczesnych języków głównego nurtu. Mam nadzieję, że wszyscy wymrą, więc wartość dowodów poprawności wzrośnie w przyszłości.
SK-logic
1

Myślę, że limity nałożone na dowody poprawności z powodu problemu zatrzymania mogą być największą barierą dla włączenia dowodów do poprawności do głównego nurtu.

Paddyslacker
źródło
8
Problem zatrzymania mówi, że nie możemy ustalić, czy jakikolwiek program zostanie zatrzymany. Programy te mogą robić dziwne rzeczy, na przykład sprawdzać każdą liczbę całkowitą, aby sprawdzić, czy jest liczbą pierwszą Mersenne. Nie robimy tego w normalnych programach!
Casebash
1
@Casebash, pytanie brzmi, czy istnieje przydatny podzbiór programów, dla których można rozwiązać problem zatrzymania. To w żadnym wypadku nie jest jasne. Czy możemy ograniczyć nasze programy, abyśmy nie mogli robić rzeczy takich jak testowanie każdej liczby całkowitej bez zniszczenia naszej zdolności do wykonywania przydatnych zadań?
Winston Ewert,
1

Jest już używany przez wszystkich. Za każdym razem, gdy używasz sprawdzania typu języka programowania, w zasadzie robisz matematyczny dowód poprawności swojego programu. Działa to już bardzo dobrze - po prostu wymaga wybrania właściwych typów dla każdej funkcji i struktury danych, której używasz. Im dokładniejszy typ, tym lepsze sprawdzanie. Istniejące typy dostępne w językach programowania mają już wystarczająco potężne narzędzia do opisania prawie każdego możliwego zachowania. Działa to w każdym dostępnym języku. C ++ i języki statyczne sprawdzają tylko czas kompilacji, podczas gdy bardziej dynamiczne języki, takie jak python, robią to po uruchomieniu programu. Kontrola nadal istnieje we wszystkich tych językach. (na przykład c ++ już obsługuje sprawdzanie skutków ubocznych w taki sam sposób, jak robi to haskell,

tp1
źródło
Jeśli chodzi o efekty uboczne w C ++, czy odnosisz się do stałej poprawności?
Winston Ewert,
tak, const + const funkcja składowa. Jeśli wszystkie funkcje składowe są stałe, wszystkich danych w obiektach nie można modyfikować.
tp1
Nadal można je modyfikować, jeśli używasz mutablelub const_cast. Z pewnością widzę połączenie, które tam rysujesz, ale smak dwóch podejść wydaje mi się raczej inny.
Winston Ewert,
Cóż, dlatego musisz go użyć - zawsze można to obejść. Ale ważne jest, jak sprawić, by kompilatory sprawdzały problemy w okolicy.
tp1