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.