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?
Odpowiedzi:
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
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
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ć.
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ę!
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.
Nie, chyba że pojawi się metoda automatycznego udowodnienia kodu bez obszernej pracy programisty.
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).
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.
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.
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.
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,
mutablelub const_cast. Z pewnością widzę połączenie, które tam rysujesz, ale smak dwóch podejść wydaje mi się raczej inny.