Używanie ściślejszego języka nie tylko przesuwa słupki celów od poprawnej implementacji do poprawnej specyfikacji. Trudno jest stworzyć coś bardzo złego, ale logicznie spójnego; dlatego kompilatory wyłapują tyle błędów.
Arytmetyka wskaźnika w takiej postaci, w jakiej jest normalnie sformułowana, jest niesłyszalna, ponieważ system typów w rzeczywistości nie oznacza, co powinien oznaczać. Możesz całkowicie uniknąć tego problemu, pracując w języku śmieci (normalne podejście, które powoduje, że płacisz również za abstrakcję). Możesz też sprecyzować, jakiego rodzaju wskaźników używasz, aby kompilator mógł odrzucić wszystko, co jest niespójne lub po prostu nie może być udowodnione, jak napisano. Takie jest podejście niektórych języków, takich jak Rust.
Skonstruowane typy są równoważne dowodom, więc jeśli napiszesz system typów, który o tym zapomina, wtedy wszystkie rzeczy się psują. Załóżmy przez chwilę, że kiedy deklarujemy typ, mamy na myśli, że potwierdzamy prawdę o tym, co znajduje się w zmiennej.
- int * x; // Fałszywe twierdzenie. x istnieje i nie wskazuje na liczbę całkowitą
- int * y = z; // Prawda tylko wtedy, gdy udowodniono, że z wskazuje na int
- * (x + 3) = 5; // Prawda tylko wtedy, gdy (x + 3) wskazuje int w tej samej tablicy co x
- int c = a / b; // Prawda tylko wtedy, gdy b jest niezerowe, na przykład: "nonzero int b = ...;"
- nullable int * z = NULL; // nullable int * to nie to samo co int *
- int d = * z; // Fałszywe twierdzenie, ponieważ z jest zerowalne
- if (z! = NULL) {int * e = z; } // Ok, ponieważ z nie ma wartości null
- wolny (y); int w = * y; // Fałszywe twierdzenie, ponieważ y już nie istnieje w w
W tym świecie wskaźniki nie mogą być zerowe. Dereferencje NullPointer nie istnieją, a wskaźniki nie muszą być nigdzie sprawdzane pod kątem nieważności. Zamiast tego „nullable int *” to inny typ, którego wartość można wyodrębnić do wartości null lub do wskaźnika. Oznacza to, że w miejscu, w którym zaczyna się założenie niepuste , albo przechodzisz rejestrowanie wyjątku, albo schodzisz do gałęzi zerowej.
W tym świecie nie występują również błędy poza zakresem. Jeśli kompilator nie może udowodnić, że jest w granicach, spróbuj przepisać, aby kompilator mógł to udowodnić. Jeśli nie może, będziesz musiał ręcznie założyć Wniebowzięcie w tym miejscu; kompilator może później znaleźć sprzeczność.
Ponadto, jeśli nie możesz mieć wskaźnika, który nie został zainicjowany, nie będziesz mieć wskaźników do niezainicjowanej pamięci. Jeśli masz wskaźnik zwolnionej pamięci, kompilator powinien go odrzucić. W Rust istnieją różne typy wskaźników, aby uzasadnić tego rodzaju dowody. Istnieją wyłącznie posiadane wskaźniki (tj .: brak aliasów), wskaźniki do głęboko niezmiennych struktur. Domyślny typ pamięci jest niezmienny itp.
Istnieje również kwestia egzekwowania rzeczywistej, dobrze zdefiniowanej gramatyki protokołów (która obejmuje elementy interfejsu), aby ograniczyć pole powierzchni wejściowej dokładnie do tego, czego się spodziewano. Rzecz „poprawności” polega na: 1) Pozbyciu się wszystkich niezdefiniowanych stanów 2) Zapewnieniu logicznej spójności . Trudność dotarcia tam ma wiele wspólnego ze stosowaniem bardzo złego oprzyrządowania (z punktu widzenia poprawności).
Właśnie dlatego dwie najgorsze praktyki to zmienne globalne i gotos. Te rzeczy uniemożliwiają ustawienie warunków przed / po / niezmiennych wokół wszystkiego. Właśnie dlatego typy są tak skuteczne. Gdy typy stają się silniejsze (ostatecznie wykorzystując typy zależne do uwzględnienia rzeczywistej wartości), stają się konstruktywnymi dowodami poprawności same w sobie; powodowanie, że niespójne programy kończą się niepowodzeniem.
Pamiętaj, że nie chodzi tylko o głupie błędy. Chodzi również o obronę bazy kodu przed sprytnymi infiltratorami. Będą przypadki, w których musisz odrzucić zgłoszenie bez przekonującego, wygenerowanego maszynowo dowodu ważnych właściwości, takich jak „postępuje zgodnie z formalnie określonym protokołem”.