Gibt es Alternativen zu Typen für die statische Analyse?

Die statische Eingabe in einer Programmiersprache kann hilfreich sein, um bestimmte Garantien beim Kompilieren durchzusetzen. Sind Typen jedoch das einzige Tool für diesen Job? Gibt es andere Möglichkeiten, Invarianten anzugeben?

Beispielsweise kann eine Sprache oder Umgebung dazu beitragen, eine Garantie hinsichtlich der Arraylänge oder der Beziehungen zwischen den Eingaben für eine Funktion durchzusetzen. Ich habe nur so etwas außerhalb eines Typsystems noch nicht gehört.

Ich habe mich auch gefragt, ob es nicht deklarative Methoden zur statischen Analyse gibt (Typen sind größtenteils deklarativ ).

Statische Typsysteme sind eine Art statische Analyse, aber es gibt viele statische Analysen, die in Typsystemen im Allgemeinen nicht codiert sind. Beispielsweise:

• Die Modellprüfung ist eine Analyse- und Überprüfungstechnik für gleichzeitige Systeme, mit der Sie nachweisen können, dass sich Ihr Programm unter allen möglichen Thread-Interleavings gut verhält.

• Die Datenflussanalyse sammelt Informationen über die möglichen Werte von Variablen, die bestimmen können, ob eine Berechnung redundant ist oder ein Fehler nicht berücksichtigt wird.

• Die abstrakte Interpretation modelliert konservativ die Auswirkungen eines Programms, in der Regel so, dass die Analyse garantiert beendet wird. Typprüfer können ähnlich wie abstrakte Interpreten implementiert werden.

• Die Trennungslogik ist eine Programmlogik (die beispielsweise im Infer- Analyzer verwendet wird), mit der Programmzustände ermittelt und Probleme wie Nullzeiger-Dereferenzen, ungültige Zustände und Ressourcenlecks identifiziert werden können.

• Kontraktbasierte Programmierung ist ein Mittel zum Spezifizieren von Vorbedingungen, Nachbedingungen, Nebenwirkungen und Invarianten. Ada hat native Unterstützung für Verträge und kann einige davon statisch überprüfen.

Optimierende Compiler führen viele kleine Analysen durch, um Zwischendatenstrukturen für die Verwendung während der Optimierung zu erstellen, z. B. SSA, Schätzungen der Inlining-Kosten, Informationen zur Anweisungspaarung usw.

Ein weiteres Beispiel für eine nicht deklarative statische Analyse ist der Hack- Typechecker, bei dem normale Kontrollflusskonstrukte den Typ einer Variablen verfeinern können:

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

Apropos "Verfeinern": Zurück in der Welt der Typsysteme paaren Verfeinerungstypen (wie sie in LiquidHaskell verwendet werden ) Typen mit Prädikaten, die garantiert für Instanzen des Typs "Verfeinert" gelten. Und abhängige Typen gehen noch einen Schritt weiter, sodass Typen von Werten abhängen können. Die "Hallo Welt" der abhängigen Typisierung ist normalerweise die Array-Verkettungsfunktion:

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

Hier ++nimmt zwei Operanden vom Typ Vec a mund Vec a n, wobei Vektoren mit Elementtyp aund Längen mund njeweils die natürlichen Zahlen sind ( Nat). Es wird ein Vektor mit demselben Elementtyp zurückgegeben, dessen Länge gleich ist m + n. Und diese Funktion beweist diese Einschränkung abstrakt, ohne die spezifischen Werte von mund zu kennen n, so dass die Längen der Vektoren dynamisch sein können.

@ JonPurdys Antwort ist besser, aber ich möchte noch ein paar Beispiele hinzufügen:

Offensichtlich:

• Syntaxprüfung

• Fusseln

Nicht offensichtlich:

• Rust ermöglicht es dem Programmierer, anzugeben, ob "Bindungen" veränderbar sind , und erzwingt diese Einschränkungen.

• Das hängt irgendwie zusammen: Einige Sprachen ermöglichen die Ausführung von Code zur Kompilierungszeit, was bedeutet, dass viele Dinge, die sonst Laufzeitfehler wären, zur Kompilierungszeit abgefangen werden können. Einige Beispiele sind Makros und Nim-Sprachprozeduren, die mit dem compileTimePragma gekennzeichnet sind .

• Logic Programmierung baut im Grunde ein Programm , indem sie Behauptungen auf.

Semistatische Typisierung:

• Facebooks Flow ermöglicht eine Mischung aus dynamischer und statischer Eingabe. Die Idee ist, dass sogar dynamischer Code implizit eingegeben wird. Mit Flow können Sie einen Server ausführen, der Ihren Code während der Ausführung überwacht, um mögliche Typfehler zu erkennen, auch wenn Sie Ihre Funktionen nicht mit Typanmerkungen versehen.

Typanalyse bedeutet nicht viel.

Es ist bekannt, dass Agda ein System vom Typ Turing-complete hat, das sehr viel anders (und viel schwieriger zu berechnen) ist als ML-Sprachen (z . B. Ocaml ).