Relation entre les contrats et la dactylographie dépendante
31
J'ai lu des articles sur les types dépendants et les contrats de programmation. D'après la majorité de ce que j'ai lu, il semble que les contrats soient des contraintes vérifiées dynamiquement et que les types dépendants soient vérifiés statiquement.
Certains documents m'ont fait penser qu'il était possible d'avoir des contrats partiellement vérifiés statiquement:
Avec cela, il semble y avoir un chevauchement important et ma catégorisation des contrats par rapport aux types dépendants commence à disparaître.
Y a-t-il quelque chose de plus profond dans l'un ou l'autre des concepts qui me manque? Ou s'agit-il vraiment de catégories floues de représentation du même concept sous-jacent?
Sur le plan pratique, les contrats sont des affirmations. Ils vous permettent de vérifier les propriétés (sans quantificateur) des exécutions individuelles d'un programme. L'idée clé au cœur de la vérification des contrats est l'idée de blâme - fondamentalement, vous voulez savoir qui est responsable d'une violation de contrat. Il peut s'agir d'une implémentation (qui ne calcule pas la valeur promise) ou de l'appelant (qui a transmis à une fonction le mauvais type de valeur).
L'idée clé est que vous pouvez suivre le blâme en utilisant le même mécanisme que les paires d'intégration-projection dans la construction de limite inverse de la théorie des domaines. Fondamentalement, vous passez de l'utilisation d'assertions à l'utilisation de paires d'assertions, dont l'une blâme le contexte du programme et l'autre blâme le programme. Ensuite, cela vous permet d'envelopper des fonctions d'ordre supérieur avec des contrats, car vous pouvez modéliser la contravariance de l'espace de fonction en échangeant la paire d'assertions. (Voir par exemple l' article de Nick Benton "Undoing Dynamic Typing" .)
Les types dépendants sont des types. Les types spécifient des règles pour déterminer si certains programmes sont acceptables ou non. En conséquence, ils n'incluent pas des choses comme la notion de blâme, car leur fonction est d'empêcher des programmes mal comportés d'exister en premier lieu. Il n'y a rien à blâmer puisque seuls les programmes bien formés sont même des énoncés grammaticaux. De manière pragmatique, cela signifie qu'il est très facile d'utiliser des types dépendants pour parler de propriétés de termes avec des quantificateurs (par exemple, qu'une fonction fonctionne pour toutes les entrées).
Ces deux vues ne sont pas identiques, mais elles sont liées. Fondamentalement, le fait est qu'avec les contrats, nous partons d'un domaine universel de valeurs et utilisons des contrats pour réduire les choses. Mais lorsque nous utilisons des types, nous essayons de spécifier des domaines de valeurs plus petits (avec une propriété souhaitée) à l'avance. Ainsi, nous pouvons connecter les deux via des familles de relations dirigées par type (c'est-à-dire des relations logiques). Par exemple, voir le récent "Blame for All" d' Ahmed, Findler, Siek et Wadler , ou "The Signification of Types: from Intrinsic to Extrinsic Semantics" de Reynolds .
Pourquoi dites-vous que les contrats sont sans quantificateur?
Radu GRIGore
3
Parce que vous ne pouvez généralement pas utiliser de tests pour établir des propriétés de fonctions universellement quantifiées, c'est tout.
Neel Krishnaswami
3
Sauf si les quantificateurs s'étendent sur des domaines finis, auquel cas ils peuvent être considérés comme de grandes conjonctions et disjonctions. Ou si vous souhaitez devenir fantaisiste, vous pouvez vérifier certains types d'instructions quantifiées, à condition que les quantiers s'étendent sur les types interrogeables de Martin Escardo (qui peuvent être infinis).
Andrej Bauer
2
@Radu: J'appelle des choses comme JML & co "logiques de programme". Les langues d'assertion des logiques de programme ne se limitent pas à être des termes issus de la langue des programmes. Cela vous permet d'exclure des choses comme les assertions non terminatives ou à effets secondaires, qui n'ont pas une bonne interprétation logique. (Cependant, de telles choses sont importantes pour la vérification des contrats - voir les travaux récents de Pucella et Tove à l'ESOP sur l'utilisation de contrats avec état et impératifs pour suivre les propriétés de linéarité.)
Le problème (assez abstrait) que les types et les contrats attaquent est "Comment s'assurer que les programmes ont certaines propriétés?". Il existe une tension inhérente entre pouvoir exprimer une classe de propriétés plus large et pouvoir vérifier qu'un programme a ou non une propriété. Les systèmes de types garantissent généralement une propriété très spécifique (le programme ne se bloque jamais de certaines manières) et ont un algorithme de vérification de type. D'un autre côté, les contrats vous permettent de spécifier une très large gamme de propriétés (disons, la sortie de ce programme est un nombre premier) mais ne sont pas fournis avec un algorithme de vérification.
Néanmoins, le fait qu'il n'y ait pas d'algorithme de vérification des contrats (qui fonctionne toujours) ne signifie pas qu'il n'y a pas presque d'algorithmes de vérification des contrats (qui ont tendance à fonctionner dans la pratique). Je vous recommande de regarder Spec # et le plugin Jessie de Frama-C . Ils travaillent tous les deux en exprimant "ce programme obéit à ce contrat" comme une déclaration dans une logique de premier ordre via la génération de conditions de vérification , puis en demandant à un SMTsolveur pour aller essayer de trouver une preuve. Si le solveur ne parvient pas à trouver une preuve, alors le programme est incorrect ou, eh bien, le solveur n'a pas réussi à trouver une preuve qui existe. (C'est pourquoi il s'agit d'un algorithme de vérification de contrat «presque».) Il existe également des outils basés sur l'exécution symbolique, ce qui signifie grosso modo que «ce programme obéit à ce contrat» est exprimé comme un tas de propositions (dans une certaine logique). Voir, par exemple, jStar .
Le travail de Flanagan tente de tirer le meilleur parti des deux mondes afin que vous puissiez rapidement vérifier les propriétés de type type, puis travailler pour le reste. Je ne connais pas vraiment les types hybrides, mais je me souviens que l'auteur avait dit que sa motivation était de trouver une solution qui nécessite moins d'annotations (que ses précédents travaux sur ESC / Java). Dans un sens, cependant, il existe également une intégration lâche entre les types et les contrats dans ESC / Java (et Spec #): lors de la vérification des contrats, le solveur est informé que la vérification de type a réussi afin qu'il puisse voir ces informations.
Les contrats peuvent être vérifiés statiquement. Si vous regardez les anciens travaux de Dana Xu sur ESC / Haskell , elle a pu implémenter la vérification complète des contrats au moment de la compilation, ne s'appuyant que sur un prouveur de théorème pour l'arithmétique. La résiliation est résolue par une simple limite de profondeur si je me souviens bien:
Les contrats et les types vous permettent de représenter les spécifications de style Hoare (conditions pré / post) sur les fonctions. Les deux peuvent être vérifiés soit statiquement au moment de la compilation, soit dynamiquement au moment de l'exécution.
Les types dépendants vous permettent d'encoder une très large gamme de propriétés dans le système de types, les types de propriétés que les programmeurs contractuels attendent. En effet, ils peuvent dépendre des valeurs du type. Les types dépendants ont tendance à être vérifiés statiquement bien que je pense que les articles que vous avez cités examinent des approches alternatives.
En fin de compte, il y a peu de différence. Je pense que c'est plus que les types dépendants sont une logique dans laquelle vous pouvez exprimer des spécifications alors que les contrats sont une méthodologie de programmation dans laquelle vous exprimez des spécifications.
Il est un peu trompeur de dire que les annotations de style Hoare peuvent être vérifiées statiquement. Si la logique est FO, comme c'est généralement le cas, alors le problème est certainement indécidable. Mais, oui, je sais que vous vouliez dire que l'on peut essayer et même réussir dans de nombreuses situations.
Radu GRIGore
1
J'avais l'impression que la génération de la preuve peut être indécidable mais la vérification d'une preuve devrait l'être. De nombreux langages de type dépendant dépendent de l'utilisateur pour fournir la valeur de preuve de l'habitation du type théorème.
Jason Reich
Vous avez raison. Mais je vis dans le monde automatisé, où l'utilisateur n'est généralement pas invité à fournir une preuve.
Le problème (assez abstrait) que les types et les contrats attaquent est "Comment s'assurer que les programmes ont certaines propriétés?". Il existe une tension inhérente entre pouvoir exprimer une classe de propriétés plus large et pouvoir vérifier qu'un programme a ou non une propriété. Les systèmes de types garantissent généralement une propriété très spécifique (le programme ne se bloque jamais de certaines manières) et ont un algorithme de vérification de type. D'un autre côté, les contrats vous permettent de spécifier une très large gamme de propriétés (disons, la sortie de ce programme est un nombre premier) mais ne sont pas fournis avec un algorithme de vérification.
Néanmoins, le fait qu'il n'y ait pas d'algorithme de vérification des contrats (qui fonctionne toujours) ne signifie pas qu'il n'y a pas presque d'algorithmes de vérification des contrats (qui ont tendance à fonctionner dans la pratique). Je vous recommande de regarder Spec # et le plugin Jessie de Frama-C . Ils travaillent tous les deux en exprimant "ce programme obéit à ce contrat" comme une déclaration dans une logique de premier ordre via la génération de conditions de vérification , puis en demandant à un SMTsolveur pour aller essayer de trouver une preuve. Si le solveur ne parvient pas à trouver une preuve, alors le programme est incorrect ou, eh bien, le solveur n'a pas réussi à trouver une preuve qui existe. (C'est pourquoi il s'agit d'un algorithme de vérification de contrat «presque».) Il existe également des outils basés sur l'exécution symbolique, ce qui signifie grosso modo que «ce programme obéit à ce contrat» est exprimé comme un tas de propositions (dans une certaine logique). Voir, par exemple, jStar .
Le travail de Flanagan tente de tirer le meilleur parti des deux mondes afin que vous puissiez rapidement vérifier les propriétés de type type, puis travailler pour le reste. Je ne connais pas vraiment les types hybrides, mais je me souviens que l'auteur avait dit que sa motivation était de trouver une solution qui nécessite moins d'annotations (que ses précédents travaux sur ESC / Java). Dans un sens, cependant, il existe également une intégration lâche entre les types et les contrats dans ESC / Java (et Spec #): lors de la vérification des contrats, le solveur est informé que la vérification de type a réussi afin qu'il puisse voir ces informations.
la source
Les contrats peuvent être vérifiés statiquement. Si vous regardez les anciens travaux de Dana Xu sur ESC / Haskell , elle a pu implémenter la vérification complète des contrats au moment de la compilation, ne s'appuyant que sur un prouveur de théorème pour l'arithmétique. La résiliation est résolue par une simple limite de profondeur si je me souviens bien:
la source
Les contrats et les types vous permettent de représenter les spécifications de style Hoare (conditions pré / post) sur les fonctions. Les deux peuvent être vérifiés soit statiquement au moment de la compilation, soit dynamiquement au moment de l'exécution.
Les types dépendants vous permettent d'encoder une très large gamme de propriétés dans le système de types, les types de propriétés que les programmeurs contractuels attendent. En effet, ils peuvent dépendre des valeurs du type. Les types dépendants ont tendance à être vérifiés statiquement bien que je pense que les articles que vous avez cités examinent des approches alternatives.
En fin de compte, il y a peu de différence. Je pense que c'est plus que les types dépendants sont une logique dans laquelle vous pouvez exprimer des spécifications alors que les contrats sont une méthodologie de programmation dans laquelle vous exprimez des spécifications.
la source