Czy istnieją alternatywy dla typów dla analizy statycznej?

Pisanie statyczne w języku programowania może być pomocne w egzekwowaniu pewnych gwarancji w czasie kompilacji - ale czy typy są jedynym narzędziem do tego zadania? Czy istnieją inne sposoby określania niezmienników?

Na przykład język lub środowisko może pomóc w egzekwowaniu gwarancji dotyczącej długości tablicy lub relacji między danymi wejściowymi do funkcji. Po prostu nie słyszałem o czymś takim poza systemem typów.

Zastanawiałem się nad tym, czy istnieją jakieś nie deklaratywne sposoby przeprowadzania analizy statycznej (typy są w większości deklaratywne ).

Systemy typu statycznego są rodzajem analizy statycznej, ale istnieje wiele analiz statycznych, które zasadniczo nie są zakodowane w systemach typów. Na przykład:

• Sprawdzanie modelu to technika analizy i weryfikacji dla współbieżnych systemów, która pozwala udowodnić, że Twój program zachowuje się dobrze we wszystkich możliwych przeplotach wątków.

• Analiza przepływu danych gromadzi informacje o możliwych wartościach zmiennych, które mogą ustalić, czy niektóre obliczenia są zbędne, czy jakiś błąd nie jest uwzględniany.

• Interpretacja abstrakcyjna konserwatywnie modeluje efekty programu, zwykle w taki sposób, że gwarantuje się zakończenie analizy - weryfikatory typu mogą być implementowane w podobny sposób, jak interpretatory abstrakcyjne.

• Logika separacji to logika programu (stosowana na przykład w analizatorze Infer ), która może być używana do wnioskowania o stanach programu i identyfikowania problemów, takich jak dereferencje wskaźnika zerowego, nieprawidłowe stany i wycieki zasobów.

• Programowanie kontraktowe jest sposobem na określenie warunków wstępnych, dodatkowych, skutków ubocznych i niezmienników. Ada ma natywne wsparcie dla kontraktów i może zweryfikować niektóre z nich statycznie.

Optymalizujące kompilatory wykonują wiele drobnych analiz w celu zbudowania pośrednich struktur danych do wykorzystania podczas optymalizacji - takich jak SSA, szacunki kosztów wewnętrznych, informacje o parowaniu instrukcji i tak dalej.

Kolejny przykład nie deklaratywnej analizy statycznej znajduje się w narzędziu sprawdzającym typ Hacka , w którym normalne konstrukcje sterowania przepływem mogą udoskonalić typ zmiennej:

$x = get_value();
if ($x !== null) {
    $x->method();    // Typechecks because $x is known to be non-null.
} else {
    $x->method();    // Does not typecheck.
}

Mówiąc o „udoskonalaniu”, w krainie systemów typów , typy udoskonalania (stosowane w LiquidHaskell ) łączą typy z predykatami, które z pewnością są zachowywane dla instancji typu „udoskonalonego”. I typy zależne wziąć to dalej, dzięki czemu typy polegać na wartości. „Witaj świecie” pisania zależnego to zwykle funkcja konkatenacji tablic:

(++) : (a : Type) -> (m n : Nat) -> Vec a m -> Vec a n -> Vec a (m + n)

Tutaj ++ma dwa operandy typu Vec a mi Vec a nbyt wektory z rodzaju elementu ai długości mi n, odpowiednio, które są liczbami naturalnymi ( Nat). Zwraca wektor o tym samym typie elementu, którego długość wynosi m + n. Ta funkcja abstrakcyjnie potwierdza to ograniczenie, nie znając konkretnych wartości mi n, więc długości wektorów mogą być dynamiczne.

Odpowiedź JonPurdy'ego jest lepsza, ale chciałbym dodać jeszcze kilka przykładów:

Oczywisty:

• sprawdzanie składni

• kłaczkowanie

Nie oczywisty:

• Rdza umożliwia programiście określenie, czy „wiązania” można modyfikować , i wymusza te ograniczenia.

• Jest to w pewnym sensie powiązane: niektóre języki umożliwiają uruchamianie niektórych kodów w czasie kompilacji, co oznacza, że ​​w czasie kompilacji można wychwycić wiele rzeczy, które w przeciwnym razie byłyby błędami środowiska wykonawczego. Niektóre przykłady to makra i procedury języka Nim oznaczone compileTimepragmą .

• Programowanie logiczne polega zasadniczo na budowaniu programu poprzez zapewnianie asercji.

Pisanie półstatyczne:

• Flow na Facebooku umożliwia hybrydę pisania dynamicznego i statycznego. Chodzi o to, że nawet kod dynamiczny jest domyślnie wpisany. Flow pozwala uruchomić serwer, który obserwuje Twój kod podczas jego działania, aby wykryć możliwe błędy pisowni, nawet jeśli nie wpisujesz adnotacji w swoich funkcjach.

Analiza typów niewiele znaczy.

Wiadomo, że Agda ma system typu Turinga kompletny, bardzo inny (i znacznie trudniejszy do obliczenia) niż języki ML (np. Ocaml ).