Dlaczego nie badamy więcej w kierunku gwarancji czasu kompilacji?

Uwielbiam wszystko, co jest czasem kompilacji i uwielbiam pomysł, że po skompilowaniu programu powstaje wiele gwarancji dotyczących jego wykonania. Mówiąc ogólnie, system typu statycznego (Haskell, C ++, ...) wydaje się dawać silniejsze gwarancje czasu kompilacji niż jakikolwiek system typu dynamicznego.

Z tego, co rozumiem, Ada idzie jeszcze dalej w zakresie sprawdzania czasu kompilacji i jest w stanie wykryć większy zakres błędów przed wykonaniem. Jest również uważany za dość bezpieczny, biorąc pod uwagę, że w pewnym momencie został wybrany do delikatnych dziedzin (gdy błędy programowania mogą kosztować ludzkie życie).

Zastanawiam się teraz: jeśli silniejsze gwarancje statyczne prowadzą do kodu, który jest bardziej udokumentowany i bezpieczny, to dlaczego nie badamy więcej w tym kierunku?

Przykładem czegoś, co wydaje się brakować, byłby język, który zamiast definiować inttyp ogólny , którego zakres jest określony przez liczbę bitów architektury podstawowej, można mieć zakresy (w poniższym przykładzie Int [a..b]opisano typ liczby całkowitej między a i b w zestawie):

a : Int [1..24]
b : Int [1..12]
a + b : Int [2..36]
a - b : Int [-11..23]
b - a : Int [-23..11]

lub (biorąc to od Ady):

a : Int [mod 24]
b : Int [mod 24]
a + b : Int [mod 24]

Ten język wybrałby najlepszy typ bazowy dla zakresu i wykonałby sprawdzanie czasu kompilacji wyrażeń. Na przykład, biorąc pod uwagę:

a : Int [-3..24]
b : Int [3..10]

następnie:

a / b

nigdy nie zostanie zdefiniowany.

To tylko przykład, ale wydaje mi się, że w czasie kompilacji możemy wymusić o wiele więcej. Dlaczego więc wydaje się tak mało badań na ten temat? Jakie są techniczne terminy opisujące ten pomysł (dzięki czemu mogę znaleźć więcej informacji na ten temat)? Jakie są granice?

Nie jestem w stanie powiedzieć, jak dużo więcej badań powinno odbywać się na ten temat, ale mogę powiedzieć, że nie jest badanie zostało zrobione, na przykład Verisoft XT Program finansowany przez rząd niemiecki.

Pojęcia, które, jak myślę, szukasz, nazywane są formalną weryfikacją i programowaniem opartym na kontraktach , przy czym ten drugi sposób jest przyjazny dla programisty. W programowaniu opartym na kontraktach najpierw piszesz kod w normalny sposób, a następnie wstawiasz do kodu tak zwane umowy . Łatwym w użyciu językiem opartym na tym paradygmacie jest Spec # firmy Microsoft Research oraz funkcjonalnie podobne, ale nieco mniej ładne rozszerzenie Code Contracts dla C #, które można wypróbować online (mają one również podobne narzędzia dla innych języków, sprawdź rise4fun ). Wspomniany „int z typem zakresu” odzwierciedla się w dwóch kontraktach w funkcji:

Contract.Requires(-3 <= a && a <= 24);
Contract.Requires( 3 <= b && b <= 10);

Jeśli chcesz wywołać tę funkcję, musisz użyć parametrów, które są spełnione, aby spełnić te kryteria, lub otrzymasz błąd czasu kompilacji. Powyższe są bardzo prostymi umowami, możesz wstawić prawie każde założenie lub wymaganie dotyczące zmiennych lub wyjątków i ich relacji, o których możesz pomyśleć, a kompilator sprawdzi, czy każde wymaganie jest objęte założeniem lub czymś, co można zapewnić, tj. Wyprowadzić z założeń. Dlatego, skąd bierze się nazwa: odbiorca stawia wymagania , osoba dzwoniąca zapewnia, że zostaną one spełnione - jak w umowie biznesowej.

$P(x_1,x_2,...,x_n)$$n$$P$jest używany. Od strony CS te dwie są kluczowymi częściami procesu - generowanie warunków weryfikacji jest trudne, a SMT stanowi problem NP-zupełny lub nierozstrzygalny, w zależności od rozważanych teorii. Istnieją nawet konkursy na solwery SMT, więc z pewnością prowadzone są badania w tym zakresie. Ponadto istnieją alternatywne podejścia do korzystania z SMT do formalnej weryfikacji, takie jak wyliczanie przestrzeni stanu, symboliczne sprawdzanie modelu, sprawdzanie modelu z ograniczeniami i wiele innych, które są również badane, choć SMT jest, afaik, obecnie najbardziej „nowoczesnym” podejściem.

Jeśli chodzi o granice ogólnej idei:

• Jak już wspomniano, udowodnienie poprawności programu jest trudnym obliczeniowo problemem, więc może się zdarzyć, że sprawdzenie czasu kompilacji programu z kontraktami (lub inną specyfikacją) zajmie naprawdę dużo czasu lub może nawet będzie niemożliwe. Najlepszym sposobem, w jaki można to zrobić, jest zastosowanie heurystyki, która działa dobrze przez większość czasu.
• Im więcej określisz w swoim programie, tym większe prawdopodobieństwo wystąpienia błędów w samej specyfikacji . Może to prowadzić do fałszywych trafień (kontrola czasu kompilacji nie powiedzie się, mimo że wszystko jest wolne od błędów) lub fałszywego wrażenia, że ​​jest bezpieczny, nawet jeśli Twój program nadal ma błędy.
• Pisanie umów lub specyfikacji to naprawdę żmudna praca, a większość programistów jest zbyt leniwa, aby to zrobić. Spróbuj napisać program w języku C # z umowami dotyczącymi kodu wszędzie, po chwili pomyślisz „no dalej, czy to naprawdę konieczne?”. Dlatego formalna weryfikacja jest zwykle stosowana tylko do projektowania sprzętu i systemów krytycznych dla bezpieczeństwa, takich jak oprogramowanie sterujące samolotami lub motoryzacja.

Ostatnią rzeczą wartą wspomnienia, która nie do końca pasuje do powyższego wyjaśnienia, jest pole o nazwie „Teoria niejawnej złożoności”, na przykład ten artykuł . Ma na celu scharakteryzowanie języków programowania, w których każdy program, który można napisać, należy do określonej klasy złożoności, na przykład P. W takim języku każdy program, który piszesz, jest automatycznie „zapewniany” jako wielomianowy czas wykonywania, który można „sprawdzić” w czasie kompilacji, po prostu kompilując program. Nie znam jednak praktycznie żadnych użytecznych wyników tych badań, ale daleko mi też do bycia ekspertem.