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

18

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 ).

Max Heiber
źródło

Odpowiedzi:

24

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.

Jon Purdy
źródło
Co to jest system typów? Zdaję sobie sprawę, że tak naprawdę nie wiem. Definicja na Wikipedii jest okrągła: en.wikipedia.org/wiki/Type_system
Max Heiber
1
@mheiber: Układ typu statycznego jest po prostu analiza statyczna że typy przypisuje (na przykład int, int -> int, forall a. a -> a) warunków (na przykład 0, (+ 1), \x -> x). Inne analizy mogą przypisywać różne właściwości niezwiązane z typem danych, na przykład skutki uboczne ( pure, io), widoczność ( public, private) lub stan ( open, closed). W praktyce wiele z tych właściwości można sprawdzić w tej samej implementacji co sprawdzanie / wnioskowanie typu, więc rozróżnienie nie jest całkowicie jednoznaczne.
Jon Purdy,
4

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.
Max Heiber
źródło
1

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 ).

Basile Starynkevitch
źródło
Agda dokłada wszelkich starań, aby nie mieć „kompletnego systemu typu Turinga”, a nawet nie mieć „kompletnego systemu terminów Turinga”.
user833970