Teoretycznie wolne od błędów programy

Przeczytałem wiele artykułów, w których stwierdzono, że kod nie może być wolny od błędów, i mówią o tych twierdzeniach:

• Problem z zatrzymaniem
• Twierdzenie Gödela o niekompletności
• Twierdzenie Rice'a

W rzeczywistości twierdzenie Rice'a wygląda jak implikacja problemu zatrzymania, a problem zatrzymania jest ściśle powiązany z twierdzeniem Gödela o niekompletności.

Czy to oznacza, że ​​każdy program będzie miał co najmniej jedno niezamierzone zachowanie? Czy oznacza to, że nie można napisać kodu, aby go zweryfikować? Co z sprawdzaniem rekurencyjnym? Załóżmy, że mam dwa programy. Oba mają błędy, ale nie mają tego samego błędu. Co się stanie, jeśli uruchomię je jednocześnie?

I oczywiście większość dyskusji dotyczyła maszyn Turinga. Co z automatyzacją ograniczoną liniowo (prawdziwe komputery)?

Nie chodzi o to, że programy nie mogą być wolne od błędów; jest to bardzo trudne do udowodnienia, że ​​są, jeśli program, który próbujesz udowodnić, jest nietrywialny.

Pamiętaj, że nie z braku prób. Systemy typów powinny zapewniać pewną pewność; Haskell ma bardzo wyrafinowany system typów, który do pewnego stopnia to robi. Ale nigdy nie można usunąć całej niepewności.

Rozważ następującą funkcję:

int add(int a, int b) { return a + b; }

Co może pójść nie tak z tą funkcją? Wiem już, co myślisz. Powiedzmy, że omówiliśmy wszystkie podstawy, takie jak sprawdzanie przepełnienia itp. Co się stanie, jeśli promień kosmiczny uderzy w procesor, powodując jego wykonanie

LaunchMissiles();

zamiast?

OK, może to trochę wymyślone. Ale nawet proste funkcje, takie jak addpowyższa funkcja, muszą działać w środowiskach, w których procesor stale zmienia konteksty, przełączając się między wieloma wątkami i rdzeniami. W takim środowisku wszystko może się zdarzyć. Jeśli masz co do tego wątpliwości, weź pod uwagę, że pamięć RAM jest niezawodna, nie dlatego, że nie zawiera błędów, ale dlatego, że ma wbudowany system do korygowania błędów bitów, które nieuchronnie występują.

Wiem, o czym myślisz. „Ale mówię o oprogramowaniu, a nie o sprzęcie”.

Istnieje wiele technik, które mogą poprawić poziom pewności, że oprogramowanie działa tak, jak powinno. Programowanie funkcjonalne jest jednym z nich. Programowanie funkcjonalne pozwala lepiej uzasadnić współbieżność. Ale programowanie funkcjonalne nie jest dowodem, podobnie jak testy jednostkowe.

Dlaczego? Ponieważ masz te rzeczy nazywane skrzynkami krawędziowymi.

A kiedy tylko wyjdziesz nieco poza prostotę return a + b, niezwykle trudno jest udowodnić poprawność programu.

Dalsza lektura
Piszą właściwe rzeczy
Wybuch Ariane 5

Najpierw ustalmy, w jakim kontekście chcesz to omówić. Pytania i odpowiedzi programistów w Stack Exchange sugerują, że najprawdopodobniej interesuje Cię istnienie narzędzi / języków w prawdziwym świecie, a nie teoretyczne wyniki i twierdzenia z zakresu informatyki .

Przeczytałem wiele artykułów, w których stwierdzono, że kod nie może być wolny od błędów

Mam nadzieję, że nie, ponieważ takie stwierdzenie jest nieprawidłowe. Chociaż powszechnie przyjmuje się, że zgodnie z moją najlepszą wiedzą i doświadczeniem większość aplikacji na dużą skalę nie jest pozbawiona błędów.

Częściej akceptowane jest to, że nie istnieje (tj. Istnienie, brak możliwości) narzędzie, które doskonale określa, czy program napisany w języku programowania Turing-complete jest całkowicie wolny od błędów.

Non-proof jest intuicyjnym rozszerzeniem problemu zatrzymania, w połączeniu z danymi obserwacyjnymi z codziennych doświadczeń.

Nie robi oprogramowanie może zrobić, że istnieją „dowody poprawności ”, które sprawdzenia, czy program spełnia odpowiednie formalne specyfikacje dla programu.

Czy to oznacza, że ​​każdy program będzie miał co najmniej jedno niezamierzone zachowanie?

Nie. Chociaż większość aplikacji ma co najmniej jeden błąd lub niezamierzone zachowanie.

Czy oznacza to, że nie można napisać kodu, aby go zweryfikować?

Nie, możesz użyć formalnych specyfikacji i asystentów ds. Weryfikacji, aby zweryfikować zgodność ze specyfikacją , ale jak pokazuje doświadczenie, w całym systemie mogą nadal występować błędy, takie jak czynniki spoza specyfikacji - tłumacz kodu źródłowego i sprzęt, a najczęściej popełniane są błędy w samych specyfikacjach.

Aby uzyskać więcej szczegółów, zobacz Coq to takie narzędzie / język / system.

Co z sprawdzaniem rekurencyjnym?

Nie wiem Nie jestem z tym zaznajomiony i nie jestem pewien, czy jest to problem obliczeniowy, czy problem optymalizacji kompilatora.

Chcę zapytać, czy to oznacza, że ​​każdy kod uzyska co najmniej jedno niezamierzone zachowanie?

Nie. Właściwe programy mogą być i są napisane. Pamiętaj, że program może być poprawny, ale jego wykonanie może się nie powieść z powodu np. Okoliczności fizycznych (jak napisał użytkownik Robert Harvey w swojej odpowiedzi tutaj ), ale jest to osobna sprawa: kod tego programu jest nadal poprawny. Mówiąc ściślej, awaria nie jest spowodowana błędem lub błędem w samym programie, ale w maszynie, która go wykonuje (*).

(*) Pożyczam definicje błędów , błędów i awarii z pola niezawodności jako, odpowiednio, wady statyczne, niepoprawny stan wewnętrzny i nieprawidłowe obserwowane zachowanie zewnętrzne zgodnie z jego specyfikacją (patrz <dowolny artykuł z tego pola>) .

Czy oznacza to, że nie jestem w stanie napisać kodu, który to sprawdzi?

Sprawdź ogólny przypadek w powyższym stwierdzeniu i masz rację.

Możesz być w stanie napisać program, który sprawdza, czy określony program X jest poprawny. Na przykład, jeśli zdefiniujesz program „hello world” jako jeden z dwiema instrukcjami w kolejności, a mianowicie print("hello world")i exitmożesz napisać program, który sprawdza, czy jego dane wejściowe to program złożony z tych dwóch instrukcji w sekwencji, raportując, czy jest to poprawny program „witaj świecie”, czy nie.

Tym, czego nie można zrobić przy użyciu bieżących sformułowań, jest napisanie programu, aby sprawdzić, czy dowolny program się zatrzymuje, co implikuje niemożność sprawdzenia poprawności w ogólnych przypadkach.

Uruchamianie dwóch lub więcej wariantów tego samego programu jest dobrze znaną techniką tolerancji błędów zwaną programowaniem w wariancie N (lub wersji N). Jest to potwierdzenie obecności błędów w oprogramowaniu.

Zazwyczaj te warianty są kodowane przez różne zespoły programistów, przy użyciu różnych kompilatorów, a czasami są wykonywane na różnych procesorach z różnymi systemami operacyjnymi. Wyniki głosowane są przed wysłaniem do użytkownika. Boeing i Airbus uwielbiają tego rodzaju architekturę.

Pozostają dwa słabe linki prowadzące do błędów w trybie wspólnym:

• Jest tylko jedna specyfikacja.
• system głosowania jest unikalny lub złożony.

Program ma pewną specyfikację i działa w pewnym środowisku.

^{(przykład promienia kosmicznego w innych odpowiedziach zmieniających się addna FireMissiles można uznać za część „środowiska”)}

Zakładając, że możesz formalnie określić zamierzone zachowanie programu (tj. Jego specyfikację) i jego środowisko, możesz czasem formalnie udowodnić, że program jest - w tym precyzyjnym sensie - wolny od błędów (więc jego zachowanie lub dane wyjściowe są zgodne z formalizacją specyfikacji w formalizacji jego środowiska).

W szczególności możesz użyć dźwiękowych analizatorów źródeł statycznych, takich jak np. Frama-C .

^{(ale obecny stan takich analizatorów nie pozwala na analizę całego programu i sprawdzenie programów na dużą skalę, takich jak kompilator GCC, przeglądarka Firefox lub jądro Linuksa; i wierzę, że takie dowody nie pojawią się za mojego życia Urodziłem się w 1959 r.)}

Jednak to, co udowodniłeś, to prawidłowe zachowanie programu w określonej specyfikacji w niektórych (klasach) środowiskach.

Praktycznie rzecz biorąc, możesz (i NASA lub ESA prawdopodobnie tego chcą) udowodnić, że niektóre oprogramowanie statków kosmicznych jest „wolne od błędów” i zawiera precyzyjną i sformalizowaną specyfikację. Ale to nie znaczy, że Twój system będzie zawsze zachowywał się tak, jak chcesz.

Mówiąc prościej, jeśli twój robot kosmiczny spełnia jakieś ET i nie określiłeś tego, nie ma sposobu, aby twój robot zachowywał się tak, jak naprawdę chcesz ...

Przeczytaj także wpisy na blogu J.Pitrat .

BTW, problem Haltinga lub twierdzenie Gödla mają prawdopodobnie zastosowanie również do ludzkiego mózgu, a nawet gatunku ludzkiego.

Czy to oznacza, że ​​każdy program będzie miał co najmniej jedno niezamierzone zachowanie?

Nie.

Problem zatrzymania mówi, że nie można napisać programu, który sprawdza, czy każdy program zatrzymuje się w określonym czasie. Nie oznacza to, że niemożliwe jest napisanie programu, który może zakwalifikować niektóre programy jako wstrzymujące, a inne jako nie zatrzymujące. Oznacza to, że zawsze będą istnieć pewne programy, których analizator zatrzymujący nie może sklasyfikować w taki czy inny sposób.

Twierdzenia Gödela o niekompletności mają podobny szary obszar do nich. Biorąc pod uwagę matematyczny system o wystarczającej złożoności, będą istnieć pewne stwierdzenia złożone w kontekście tego systemu, których prawdziwości nie można ocenić. Nie oznacza to, że matematycy muszą zrezygnować z idei dowodu. Dowód pozostaje kamieniem węgielnym matematyki.

Niektóre programy można udowodnić, że są poprawne. To nie jest łatwe, ale można to zrobić. Taki jest cel formalnego dowodzenia twierdzeń (część metod formalnych). Uderzają tu twierdzenia Gödela o niekompletności: Nie wszystkie programy można udowodnić, że są poprawne. Nie oznacza to, że stosowanie metod formalnych jest całkowicie bezcelowe, ponieważ niektóre programy rzeczywiście można formalnie udowodnić, że są poprawne.

Uwaga: Metody formalne wykluczają możliwość uderzenia promienia kosmicznego w procesor i wykonania launch_missiles()zamiast niego a+b. Analizują programy w kontekście abstrakcyjnej maszyny, a nie prawdziwych maszyn, które podlegają zdenerwowaniu pojedynczym zdarzeniem, takim jak promień kosmiczny Roberta Harveya.

Istnieje tutaj wiele dobrych odpowiedzi, ale wszystkie wydają się omijać punkt krytyczny, a mianowicie: wszystkie te twierdzenia mają podobną strukturę i mówią podobne rzeczy, a to, co mówią, nie jest „prawdopodobnie niemożliwe jest poprawne napisanie programy”(dla niektórych wartości określonej w«poprawne»i«program», który zmienia się w każdym przypadku), ale co zrobić, powiedzieć,«że to niemożliwe, aby zapobiec ktoś pisze błędny program, który nie może okazać się niewłaściwe»( itp).

Biorąc pod uwagę konkretny przykład problemu zatrzymania, różnica staje się wyraźniejsza: oczywiście istnieją programy, które można zatrzymać, a inne programy, które prawdopodobnie nigdy się nie zatrzymają. To, że istnieje trzecia klasa programów, których zachowania nie można ustalić w żaden sposób, nie stanowi problemu, jeśli wszystko, co chcemy zrobić, to napisać program, który da się zatrzymać, ponieważ możemy po prostu uniknąć pisania programu, który należy do tej klasy.

To samo dotyczy twierdzenia Rice'a. Tak, dla każdej nietrywialnej własności programu możemy napisać program, w którym ta właściwość nie będzie ani sprawdzona, ani prawdziwa, ani fałszywa; możemy również uniknąć pisania takiego programu, ponieważ jesteśmy w stanie ustalić, czy program jest możliwy do udowodnienia.

Moja odpowiedź będzie z perspektywy realnego biznesu i wyzwań, przed którymi stoi każdy zespół programistów. To, co widzę w tym pytaniu i wiele odpowiedzi, naprawdę dotyczy kontrolowania wad.

Kod może być wolny od błędów. Pobierz dowolny przykładowy kod „Hello World” dla dowolnego języka programowania i uruchom go na platformie, na której jest przeznaczony, i będzie działał konsekwentnie i dawał pożądane wyniki. Kończą się teorie na temat niemożności, by kod był wolny od błędów.

Potencjalne błędy pojawiają się, gdy logika staje się bardziej złożona. Prosty przykład Hello World nie ma logiki i za każdym razem robi to samo. Natychmiast po dodaniu dynamicznego działania opartego na logice wprowadza się złożoność, która prowadzi do błędów. Sama logika może być wadliwa lub dane wprowadzane do logiki mogą się różnić w sposób, w jaki logika nie obsługuje.

Nowoczesna aplikacja zależy również od bibliotek wykonawczych, CLR, oprogramowania pośredniego, bazy danych itp., Które - choć ogólnie oszczędzają czas programowania - są również warstwami, w których mogą występować błędy w tych warstwach, które nie są wykrywane podczas testowania i testowania UAT i do produkcji.

Wreszcie, łańcuch aplikacji / systemów, w których aplikacja zużywa dane, które zasilają jej logikę, to wszystkie źródła potencjalnych błędów w ich logice lub w oprogramowaniu, które układa logikę na wierzchu lub w systemach, w których pobiera dane.

Deweloperzy nie mają 100% kontroli nad każdym ruchomym elementem wspierającym logikę ich aplikacji. W rzeczywistości nie kontrolujemy wiele. Dlatego testowanie jednostkowe jest ważne, a zarządzanie konfiguracją i zmianami to ważne procesy, których nie możemy ignorować ani być leniwi / niedbali.

Udokumentowane umowy między aplikacją, która zużywa dane ze źródła, na które nie masz wpływu, które określają konkretny format i specyfikacje przesyłanych danych, a także wszelkie ograniczenia lub ograniczenia, które system przyjmuje, że system źródłowy jest odpowiedzialny za zapewnienie, że dane wyjściowe mieszczą się w zakresie te granice.

W rzeczywistej aplikacji inżynierii oprogramowania nie będziesz w stanie sprawić, by latała, wyjaśniając biznesowi, dlaczego teoretycznie aplikacje nie mogą być wolne od błędów. Dyskusje na ten temat między technologią a biznesem nigdy nie będą się odbywać, chyba że w następstwie awarii technologicznej, która wpłynęła na zdolność firmy do zarabiania pieniędzy, zapobiegania utracie pieniędzy i / lub utrzymywania ludzi przy życiu. Odpowiedź na „jak to się może zdarzyć” nie może być „pozwólcie mi wyjaśnić tę teorię, abyście rozumieli”.

Pod względem ogromnych obliczeń, które teoretycznie mogą trwać wiecznie, aby wykonać obliczenia i uzyskać wynik, aplikacja, która nie może zakończyć i powrócić z wynikiem - to jest błąd. Jeśli charakter obliczeń jest taki, że jest bardzo czasochłonny i intensywny obliczeniowo, przyjmujesz to żądanie i przekazujesz użytkownikowi informacje zwrotne, w jaki sposób / kiedy może on uzyskać wynik, i uruchamiasz równoległe wątki, aby się na nim zgubić. Jeśli musi to nastąpić szybciej, niż można to zrobić na jednym serwerze i jest to wystarczająco ważne z biznesowego punktu widzenia, należy skalować go na tyle systemów, ile potrzeba. Właśnie dlatego chmura jest bardzo atrakcyjna, a możliwość spinania węzłów w celu podjęcia pracy i spinania ich po zakończeniu.

Jeśli istnieje możliwość otrzymania żądania, że ​​żadna ilość mocy obliczeniowej nie jest w stanie ukończyć, nie powinna spędzać czasu w nieskończoności z procesem biznesowym czekającym na odpowiedź na pytanie, co według firmy jest skończonym problemem.

Nie wierzę, że kod jest w 100% wolny od błędów, ponieważ kod nigdy nie jest naprawdę gotowy. Zawsze możesz poprawić to, co piszesz.

Programowanie jest dziedziną nauki i matematyki, w którym to przypadku oba są nieograniczone. Wspaniałą rzeczą w byciu programistą jest to, że nasza praca jest nieograniczona.

Istnieje ponad tysiąc sposobów na napisanie jednego wiersza kodu. Chodzi o to, aby napisać najbardziej zoptymalizowaną wersję tego wiersza kodu, ale może to nie być wolne od błędów. Bezbłędny odnosi się do idei, że Twój kod jest niezniszczalny, a cały kod można złamać w pewnym stopniu lub w dowolnej metodzie.

Czy kod może być wydajny? Tak.
Czy kod można optymalizować bez końca? Tak.
Czy kod może być wolny od błędów? Nie, po prostu nie znalazłeś jeszcze sposobu, aby go złamać.
Biorąc to pod uwagę, jeśli starasz się poprawić siebie i swoje praktyki pisania kodu, Twój kod będzie trudny do złamania.