Co wiemy o możliwych do udowodnienia poprawnych programach?

Coraz większa złożoność programów komputerowych i coraz ważniejsza pozycja komputerów w naszym społeczeństwie sprawia, że ​​zastanawiam się, dlaczego nadal nie używamy zbiorowo języków programowania, w których musisz formalnie udowodnić, że kod działa poprawnie.

Uważam, że termin ten jest „kompilatorem certyfikującym” (znalazłem go tutaj ): kompilatorem kompilującym język programowania, w którym nie tylko trzeba napisać kod, ale także podać specyfikację kodu i udowodnić, że kod jest zgodny z specyfikacji (lub użyj do tego automatycznego automatu).

Podczas przeszukiwania Internetu znalazłem tylko projekty, które albo używają bardzo prostego języka programowania, albo projekty, które zakończyły się niepowodzeniem, które próbują dostosować nowoczesne języki programowania. To prowadzi mnie do mojego pytania:

Czy są jakieś kompilatory certyfikujące implementujące w pełni rozwinięty język programowania, czy też jest to bardzo trudne / teoretycznie niemożliwe?

Dodatkowo mam jeszcze zobaczyć każdy klasa złożoności udziałem udowodnić programy, takie jak „klasie wszystkich językach rozstrzygalne przez maszynę Turinga, dla którego istnieje dowód, że ta maszyna Turinga zatrzymanie”, które będę nazywał $ProvableR$ , jako analogiczny do $R$ , zestaw języków rekurencyjnych.

Widzę zalety studiowania takiej klasy złożoność: na przykład, w przypadku $ProvableR$ Zahamowanie problemem jest rozstrzygalne (nawet przypuszczenie $ProvableRE$ określony w sposób oczywisty byłoby największa klasa języków, dla których jest to rozstrzygalne). Ponadto wątpię, abyśmy wykluczyli jakiekolwiek praktycznie przydatne programy: kto używałby programu, gdy nie można udowodnić, że się zakończył?

Moje drugie pytanie brzmi:

Co wiemy o klasach złożoności, które wymagają, aby ich języki zawierały pewne właściwości?

„Kompilator certyfikujący” zwykle oznacza coś nieco innego: oznacza, że ​​masz kompilator, który może udowodnić, że kod maszynowy, który emituje poprawnie, implementuje semantykę wysokiego poziomu. Oznacza to, że nie ma błędów kompilatora. Programy, które ludzie przekazują kompilatorowi, mogą nadal być niepoprawne, ale kompilator wygeneruje poprawną wersję niewłaściwego programu z kodem maszynowym. Największą historią sukcesu w tym zakresie jest zweryfikowany kompilator CompCert , który jest kompilatorem dużej części C.

Sam kompilator Compcert jest programem z potwierdzeniem poprawności (wykonanym w Coq), co gwarantuje, że jeśli wygeneruje kod programu, będzie poprawny (w odniesieniu do semantyki operacyjnej asemblera i C, z której korzystali projektanci CompCert). Wysiłek, aby sprawdzić te rzeczy na maszynie jest dość duży; zazwyczaj dowód poprawności będzie wynosić od 1x do 100x rozmiaru weryfikowanego programu. Pisanie programów i proofów sprawdzanych maszynowo to nowa umiejętność, której musisz się nauczyć - nie jest to matematyka ani programowanie jak zwykle, ale zależy to od tego, czy potrafisz dobrze robić obie rzeczy. Wydaje się, że zaczynasz od zera, jakbyś był początkującym programistą.

Nie istnieją jednak żadne specjalne teoretyczne bariery. Jedyną rzeczą w tym zakresie jest twierdzenie o wielkości Bluma, że dla każdego języka, w którym wszystkie programy są całkowite, można znaleźć program w ogólnym języku rekurencyjnym, który będzie co najmniej wykładniczo większy, gdy zostanie zaprogramowany w całym języku. Sposobem na zrozumienie tego wyniku jest to, że cały język koduje nie tylko program, ale także dowód zakończenia. Możesz więc mieć krótkie programy z długoterminowymi dowodami zakończenia. Nie ma to jednak większego znaczenia w praktyce, ponieważ zawsze będziemy pisać programy z możliwymi do zarządzania dowodami zakończenia.

EDYCJA: Dai Le poprosił o pewne opracowanie ostatniego punktu.

Jest to głównie twierdzenie pragmatyczne, oparte na fakcie, że jeśli rozumiesz, dlaczego program działa, to jest mało prawdopodobne, aby przyczyną były niezmiennie miliony niezmiennych stron. (Najdłuższe niezmienniki, których użyłem, mają kilka stron, a chłopcy sprawiają, że recenzenci narzekają! Oczywiście również, ponieważ niezmiennik jest powodem, dla którego program działa bez narracji, która pomaga ludziom to zrozumieć.)

Ale są też powody teoretyczne. Zasadniczo nie znamy zbyt wielu sposobów systematycznego opracowywania programów, których dowody poprawności są bardzo długie. Główną metodą jest (1) wzięcie logiki, w której dowodzisz poprawności, (2) znalezienie właściwości, której nie można bezpośrednio wyrazić w tej logice (dowody spójności są typowym źródłem), oraz (3) znalezienie programu, którego dowód poprawności opiera się na rodzinie wyraźnych konsekwencji niewyrażalnej własności. Ponieważ (2) jest niewyrażalny, oznacza to, że dowód każdej wyraźnej konsekwencji musi być wykonany niezależnie, co pozwala wysadzić rozmiar dowodu poprawności. Jako prosty przykład zauważ, że w logice pierwszego rzędu z relacją nadrzędną nie można wyrazić relacji przodka.$k$$k$$k$

Wyrafinowane podejście do tego tematu nazywa się „matematyką odwrotną” i jest to badanie, które aksjomaty są wymagane do udowodnienia danych twierdzeń. Nie wiem zbyt wiele na ten temat, ale jeśli opublikujesz pytanie dotyczące jego zastosowania w CS, jestem pewien, że przynajmniej Timothy Chow i prawdopodobnie kilka innych osób będzie w stanie opowiedzieć ci interesujące rzeczy.

Myślę, że odpowiedź na pierwsze pytanie jest taka, że ​​generalnie jest to zbyt dużo pracy przy użyciu obecnych narzędzi. Aby uzyskać wrażenie, proponuję spróbować udowodnić poprawność sortowania bąbelkowego w Coq (lub jeśli wolisz trochę więcej wyzwań, skorzystaj z szybkiego sortowania). Nie sądzę, że uzasadnione jest oczekiwanie od programistów pisania zweryfikowanych programów, o ile udowodnienie poprawności takich podstawowych algorytmów jest tak trudne i czasochłonne.

To pytanie jest podobne do pytania, dlaczego matematycy nie piszą formalnych dowodów weryfikowalnych przez weryfikatory dowodów? Napisanie programu z formalnym dowodem poprawności oznacza udowodnienie matematycznego twierdzenia o pisanym kodzie, a odpowiedź na to pytanie dotyczy również twojego pytania.

Nie oznacza to, że nie było udanych przypadków zweryfikowanych programów. Wiem, że istnieją grupy, które dowodzą poprawności systemów, takich jak hypervisor Microsoft . Pokrewnym przypadkiem jest zweryfikowany kompilator C firmy Microsoft . Jednak ogólnie rzecz biorąc, obecne narzędzia wymagają wielu prac rozwojowych (w tym ich aspektów SE i HCI), zanim staną się przydatne dla ogólnych programistów (i matematyków).

Jeśli chodzi o ostatni akapit odpowiedzi Neela na temat wzrostu wielkości programu dla języków z tylko całkowitymi funkcjami, w rzeczywistości łatwo jest udowodnić jeszcze więcej (jeśli dobrze to zrozumiałem). Uzasadnione jest oczekiwanie, że składnią dowolnego języka programowania będzie ce, a zestawem całkowitych funkcji obliczeniowych nie będzie ce, więc dla każdego języka programowania, w którym wszystkie programy są sumy, istnieje całkowita funkcja obliczalna, której żaden program nie może obliczyć ( dowolnego rozmiaru) w tym języku.

$AC^0$$AC^0$-kompletny dla klasy złożoności, dlatego zawiera wszystkie problemy w klasie złożoności i może udowodnić całość tych programów. Związek między dowodami a teorią złożoności jest badany pod kątem złożoności dowodów, jeśli jesteś zainteresowany , zobacz najnowszą książkę SA Cooka i P. Nguyena „ Logiczne podstawy dowodu złożoności ”. (Dostępny jest szkic z 2008 roku.) Tak więc podstawową odpowiedzią jest, że dla wielu klas „Proviable C = C”.

$PA$$\epsilon_0$$T$$PA^2$$F$$I\Sigma_1$

Ale nie wydaje mi się, aby to znaczyło wiele w kontekście weryfikacji programu, ponieważ istnieją również programy, które rozszerzają obliczanie tej samej funkcji, ale nie możemy udowodnić, że oba programy obliczają tę samą funkcję, tj. Programy są rozszerzone równe, ale nie celowo. (Jest to podobne do Gwiazdy Porannej i Gwiazdy Wieczornej.) Ponadto łatwo jest zmodyfikować dany program dający się w całości udowodnić, aby uzyskać taki, którego teoria nie jest w stanie udowodnić swojej całości.

$P$$n$$n$$P$algorytm faktoryzacji z dowodu. (Są też badacze, którzy starają się maksymalnie zautomatyzować pierwsze podejście, ale sprawdzanie interesujących nietrywialnych właściwości programów jest trudne obliczeniowo i nie może być całkowicie zweryfikowane bez fałszywych wyników pozytywnych i negatywnych).

To, o co pytasz w pierwszym pytaniu, jest czasem nazywane „kompilatorem weryfikującym”, a kilka lat temu Tony Hoare zaoferował to jako wielkie wyzwanie dla badań komputerowych . Do pewnego stopnia to już istnieje i jest aktywnie wykorzystywane w narzędziach takich jak przysłowiowa twierdzenie Coqa , które organizują problem za pomocą teorii typów i zasady twierdzeń jak typy („ Curry-Howard ”).

EDYCJA: chciałem po prostu podkreślić „do pewnego stopnia”. Nie jest to dalekie od rozwiązania problemu, ale sukces Coq daje nadzieję, że nie jest to marzenie o fajce.

Narzędzie sprawdzające poprawność programu jest czasem nazywane weryfikatorem programu. W tym kontekście „poprawne” zwykle oznacza dwie rzeczy: że program nigdy nie wytwarza określonych wyników (błąd segmentacji, wyjątek NullPointerException itp.) I że program zgadza się ze specyfikacją.

Kod i specyfikacja mogą się zgadzać i nadal być postrzegane jako błędne. W pewnym sensie poproszenie programistów o napisanie specyfikacji jest jak poproszenie dwóch programistów o rozwiązanie problemu. Jeśli dwie implementacje się zgadzają, masz większą pewność, że są w porządku. W innym sensie specyfikacje są jednak lepsze niż drugie wdrożenie. Ponieważ specyfikacja nie musi być wydajna ani nawet wykonywalna, może być o wiele bardziej zwięzła, a zatem trudniejsza do popełnienia błędu.

Mając to na uwadze, polecam przyjrzeć się weryfikatorowi programu Spec # .

W ogólnym przypadku niemożliwe jest utworzenie algorytmu, który potwierdza, czy algorytm jest równoważny specyfikacji. To nieformalny dowód:

Prawie wszystkie języki programowania są kompletne. Dlatego każdy język wybrany przez TM może być również określony przez program napisany w tym języku.

$Equivalence/TM$

$Equivalence/TM$$Non-emptiness/TM$$Emptiness/TM$$Emptiness/TM$$Equivalence/TM$$Equivalence/TM$jest również niedopuszczalne. Dlatego możesz użyć algorytmu, niezależnie od tego, czy dwie maszyny nie są równoważne, ale nie możesz być pewien, czy są one równoważne, lub nie masz wystarczającego czasu na algorytm.

Jest to jednak tylko ogólny przypadek. Możliwe jest, że możesz zdecydować, czy specyfikacje są równoważne z programem, rozwiązując bardziej zrelaksowaną wersję problemu. Na przykład możesz zbadać tylko kilka danych wejściowych lub powiedzieć, że oba programy są równoważne z pewną niepewnością. Na tym właśnie polega testowanie oprogramowania.

Jeśli chodzi o pozostałe pytania:

Uwaga: Ta część została zredagowana w celu wyjaśnienia. Okazuje się, że popełniłem błąd, którego starałem się uniknąć, przepraszam.

$TrueR$$TrueR \subseteq R$

$ProvableR = TrueR$$ProvableR \subset TrueR$$TrueR \subset ProvableR$$A \epsilon TrueR$$A$$A$$A \epsilon ProvableR$

Nieformalnie można to podsumować następująco: Nie wiesz, że język jest rozstrzygalny, dopóki go nie udowodnisz. Więc jeśli w systemie formalnym masz wiedzę, że język jest rozstrzygalny, wiedza ta może również służyć jako dowód na to. Dlatego nie można jednocześnie mieć wiedzy, że język jest rozstrzygalny i nie można tego udowodnić, więc te dwa stwierdzenia wzajemnie się wykluczają.

$R$$ProvableR$$ProvableR \subset R$$R$

@Kaveh podsumowuje to najlepiej: sprawdzalność zawsze oznacza sprawdzalność w jakimś systemie / teorii i ogólnie nie pokrywa się z prawdą.

To samo dotyczy każdej innej klasy złożoności: aby określić członkostwo, potrzebujesz najpierw dowodu. Dlatego uważam, że twoje drugie pytanie jest zbyt ogólne, ponieważ zawiera nie tylko teorię złożoności, ale także teorię obliczeń, w zależności od właściwości, którą chcesz mieć w języku.

Poniższa klasyczna monografia analizuje prawie dokładnie drugie pytanie:

Hartmanis, J. Możliwe obliczenia i możliwe do udowodnienia właściwości złożoności , CBMS-NSF Regional Conference Series in Applied Mathematics, 30. Society for Industrial and Applied Mathematics (SIAM), Philadelphia, Pa., 1978.

$\{L(M_i) | T_i(n) \leq T(n) \text{ is provable in F}\}$$M_i$$T_i(n)$$M_i$$n$

$T(n) \geq n \log(n)$$g(n) \geq 1$$F$$TIME[T(n)] \subsetneq TIME[T(n) g(n)]$

Twierdzenie 6.5: Istnieją obliczalne monotonicznie rosnące granice czasu dla których - .$T(n)$$F$$TIME[T(n)] \neq TIME[T(n)]$

Twierdzenie 6.14: Dla dowolnego obliczalnego , .$T(n) \geq n \log(n)$$TIME[T(n)] = \{ L(M_i) | \text{F proves} (\exists j)[L(M_j) = L(M_i) \wedge T_j(n) \leq T(n)] \}$

Jednak w przypadku przestrzeni kosmicznej sytuacja jest lepiej kontrolowana:

Twierdzenie 6.9: (1) Jeśli można konstruować w przestrzeni, to - .$s(n) \geq n$$SPACE[s(n)] = F$$SPACE[s(n)]$

(2) Jeśli - ( ), istnieje do zbudowania w przestrzeni, tak że .S P A C E [ S ( n ) ] S ( n ) ≥ n s ( n ) S P A C E [ S ( n ) ] = S P A C E [ s ( n ) $SPACE[S(n)]=F$$SPACE[S(n)]$$S(n) \geq n$$s(n)$$SPACE[S(n)]=SPACE[s(n)]$

Pytanie musi zostać postawione poprawnie. Na przykład nikt nigdy nie chce wiedzieć, czy rzeczywisty program ukończyłby daną nieskończoną pamięć i jakieś środki dostępu do niej (być może operacja przesunięcia adresu bazowego o jakąś liczbę). Twierdzenie Turinga nie ma znaczenia dla programowania poprawności w jakimkolwiek konkretnym sensie, a ludzie, którzy przytaczają go jako barierę dla weryfikacji programu, mylą dwie całkiem różne rzeczy. Kiedy inżynierowie / programiści mówią o poprawności programu, chcą wiedzieć o właściwościach skończonych. Dotyczy to również matematyków, którzy są zainteresowani tym, czy coś da się udowodnić. List Godela http://vyodaiken.com/2009/08/28/godels-lost-letter/ wyjaśnia to bardziej szczegółowo.

Mianowicie, oznaczałoby to oczywiście, że pomimo nierozstrzygalności Entscheidungsproblem, umysłową pracę matematyka dotyczącą pytań typu „tak lub nie” można całkowicie zastąpić maszyną. W końcu należałoby po prostu wybrać liczbę naturalną n tak dużą, że gdy maszyna nie daje wyniku, nie ma sensu więcej myśleć o problemie.

Może być niewykonalne zbadanie ogromnego zestawu stanów programu wykonującego się na rzeczywistym komputerze i wykrycie złych stanów, nie ma teoretycznego powodu, dla którego nie można tego zrobić. W tej dziedzinie poczyniono znaczne postępy - na przykład patrz http://www.cs.cornell.edu/gomes/papers/SATSolvers-KR-book-draft-07.pdf (podziękowania dla Neila Immermana za mówiąc mi o tym)

Innym i trudniejszym problemem jest dokładne określenie, jakie właściwości ma mieć program, aby był poprawny.