Existe-t-il des alternatives aux types pour l'analyse statique?

La saisie statique dans un langage de programmation peut être utile pour appliquer certaines garanties au moment de la compilation, mais les types sont-ils le seul outil pour ce travail? Existe-t-il d'autres façons de spécifier des invariants?

Par exemple, un langage ou un environnement peut aider à appliquer une garantie concernant la longueur du tableau ou les relations entre les entrées d'une fonction. Je n'ai tout simplement pas entendu parler de quelque chose comme ça en dehors d'un système de type.

Une question connexe à laquelle je me demandais est s'il existe des moyens non déclaratifs de faire une analyse statique (les types sont déclaratifs, pour la plupart ).

Les systèmes de types statiques sont une sorte d'analyse statique, mais il existe de nombreuses analyses statiques qui ne sont généralement pas codées dans les systèmes de types. Par exemple:

• La vérification de modèle est une technique d'analyse et de vérification pour les systèmes concurrents qui vous permet de prouver que votre programme se comporte bien sous tous les entrelacements de threads possibles.

• L'analyse du flux de données rassemble des informations sur les valeurs possibles des variables, ce qui peut déterminer si certains calculs sont redondants ou si certaines erreurs ne sont pas prises en compte.

• L'interprétation abstraite modélise de manière conservatrice les effets d'un programme, généralement de telle sorte que l'analyse est garantie de se terminer - les vérificateurs de type peuvent être implémentés d'une manière similaire aux interprètes abstraits.

• La logique de séparation est une logique de programme (utilisée par exemple dans l' analyseur Infer ) qui peut être utilisée pour raisonner sur les états du programme et identifier les problèmes tels que les déréférences de pointeur nul, les états non valides et les fuites de ressources.

• La programmation par contrat est un moyen de spécifier les conditions préalables, les postconditions, les effets secondaires et les invariants. Ada a un support natif pour les contrats et peut vérifier certains d'entre eux statiquement.

Les compilateurs d'optimisation effectuent de nombreuses petites analyses afin de créer des structures de données intermédiaires à utiliser lors de l'optimisation, telles que SSA, les estimations des coûts en ligne, les informations d'appariement des instructions, etc.

Un autre exemple d'analyse statique non déclarative se trouve dans le vérificateur de type Hack , où les constructions de flux de contrôle normales peuvent affiner le type d'une variable:

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

Et en parlant de «raffinage», de retour au pays des systèmes de types , les types de raffinement (tels qu'utilisés dans LiquidHaskell ) associent des types avec des prédicats qui sont garantis pour les instances du type «raffiné». Et les types dépendants vont plus loin, permettant aux types de dépendre des valeurs. Le «bonjour» du typage dépendant est généralement la fonction de concaténation de tableau:

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

Ici, ++prend deux opérandes de type Vec a met Vec a n, étant des vecteurs de type d'élément aet de longueurs met nrespectivement, qui sont des nombres naturels ( Nat). Il renvoie un vecteur avec le même type d'élément dont la longueur est m + n. Et cette fonction prouve cette contrainte de manière abstraite, sans connaître les valeurs spécifiques de met n, donc les longueurs des vecteurs peuvent être dynamiques.

@ La réponse de JonPurdy est meilleure, mais j'aimerais ajouter quelques exemples supplémentaires:

Évident:

• vérification de la syntaxe

• peluches

Pas évident:

• Rust permet au programmeur de spécifier si les "liaisons" sont modifiables et applique ces contraintes.

• Ceci est en quelque sorte lié: certains langages permettent d'exécuter du code au moment de la compilation, ce qui signifie que de nombreuses choses qui seraient autrement des erreurs d'exécution peuvent être détectées au moment de la compilation. Quelques exemples sont les macros et les procédures en langage Nim marquées du compileTimepragma .

• La programmation logique consiste essentiellement à créer un programme en fournissant des assertions.

Typage semi-statique:

• Facebook's Flow permet un hybride entre la frappe dynamique et statique. L'idée est que même le code dynamique est implicitement typé. Flow vous permet d'exécuter un serveur qui surveille votre code pendant qu'il s'exécute pour détecter d'éventuelles erreurs de type, même si vous n'annotez pas vos fonctions.

L'analyse de type ne signifie pas grand-chose.

Agda est connu pour avoir un système de type Turing-complet, très différent (et beaucoup plus difficile à calculer) que les langages ML (par exemple Ocaml ).