Bibliographie & annexes
Présentation
English
RÉSUMÉ
Un assistant de preuve est un logiciel interactif permettant à son utilisateur de construire des démonstrations de façon semi-automatique, tout en garantissant la correction de ces démonstrations. Ce type d'outil est utile à la vérification de logiciel critique. Cet article présente Coq, assistant de preuve développé en coordination avec l’Inria, à travers un exemple de vérification d'une fonction de tri. Ensuite sont décrits quelques domaines d'applications, notamment la sûreté du logiciel et la recherche en informatique et en mathématiques. Coq est considéré comme un des outils les plus fiables pour la validation du logiciel, ce qui s’explique par les fondements théoriques de cet outil et son évolution depuis plus de 30 ans de recherche et de développement.
Lire cet article issu d'une ressource documentaire complète, actualisée et validée par des comités scientifiques.
Lire l’articleAuteur(s)
-
Sandrine Blazy : Université de Rennes 1, IRiSA, CNRS
-
Pierre Castéran : Univ. Bordeaux, LaBRI, CNRS, INP Bordeaux
-
Hugo Herbelin : Chercheur Inria Paris
INTRODUCTION
Face à l’importance croissante des composants informatiques – logiciels et matériels – dans des domaines critiques aussi divers que transports, énergie, santé, finance, etc., le besoin de composants sûrs se fait de plus en plus impérieux.
Par exemple, l’exécution d’un programme doit se faire sans erreur dans les conditions d’application prévues : absence d’erreur à l’exécution ou de bouclage non désiré, conformité à une spécification fonctionnelle.
Or nous savons, depuis Turing , qu’aucun algorithme ne peut automatiquement prendre en donnée un programme quelconque et rendre en un temps fini un diagnostic de correction. Par conséquent, seule une partie de la tâche de certification d’un logiciel peut être automatisée. Pour le reste, on peut recourir à des outils interactifs, où la preuve – souvent complexe – de correction doit être guidée par l’utilisateur.
Les assistants de preuve sont des logiciels interactifs permettant à leur utilisateur de prouver des théorèmes en le déchargeant des tâches fastidieuses et susceptibles d’être entachées d’erreurs. Outre cette fonction d’assistance à l’écriture de démonstrations, ces logiciels vérifient que toutes les preuves construites sont complètes et respectent toutes les lois de la logique.
Par « théorème », nous entendons toute sorte d’énoncé concernant soit le domaine mathématique, soit le comportement de programmes écrits dans un langage donné. Citons deux exemples, prouvés en Coq :
« Toute carte planaire peut être coloriée avec au plus quatre couleurs. »
Le compilateur CompCert garantit que tout code exécutable qu’il génère se comporte exactement comme le programme source C dont il est issu .
Coq est un logiciel puissant et complexe, en constante évolution. Dans cet article, nous proposons en première partie une introduction sur un exemple très simple de preuve d’un petit programme fonctionnel. Une deuxième partie présente quelques applications de taille réelle. Nous terminerons par des indications sur l’apprentissage de Coq et des précisions sur l’évolution de cet outil.
L'expertise technique et scientifique de référence
DOI (Digital Object Identifier)
Cet article fait partie de l’offre
Technologies logicielles Architectures des systèmes
(240 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive
Présentation
Apprendre Coq
English
4. Évolution
Le système Coq, dans son état actuel, est le résultat de plus de trente ans de recherches et d’attention aux besoins de ses utilisateurs. Une connaissance très légère de cette évolution permet de comprendre des caractéristiques qui pourraient paraître complexes ou étranges.
4.1 Outil issu de la recherche fondamentale
Issue des travaux de Thierry Coquand et Gérard Huet sur le Calcul des Constructions (en anglais CoC), eux-mêmes s’appuyant sur plusieurs décennies de recherche en logique et en informatique fondamentale et appliquée, la première version du système Coq, alors appelée CONSTR, date de décembre 1984. Quelques versions expérimentales plus tard, ce sera cependant le nouveau Calcul des Constructions Inductives (en anglais CIC) de Thierry Coquand et Christine Paulin-Mohring qui servira dès 1989 de fondation. Le système CONSTR, basé sur le CoC, devient alors Coq, basé sur le CIC.
HAUT DE PAGE4.2 Outil actuel
Coq voit s’ajouter au fil du temps de nombreuses extensions, motivées par des besoins concrets, étudiées par des chercheurs qui en isolent la substantifique moelle scientifique. Ce fut par exemple l’ajout, dès 1988, d’un mécanisme d’extraction automatique des preuves et des programmes Coq vers les langages compilés OCaml, Haskell et Scheme, ou l’ajout en 1999, d’une notion de type coinductif, duale de celle de type inductif et fort utile pour représenter les flux de données infinis. Sans chercher à l’exhaustivité, on pourra aussi citer pêle-mêle divers points qui font de Coq un système généraliste utilisé au quotidien : des bibliothèques, une large panoplie de méthodes de preuves programmables, que l’on appelle des tactiques, des interfaces graphiques, des mécanismes de notations et d’inférence automatique de l’information implicite, ce qui permet d’écrire des spécifications « comme sur le papier », sans parler de nombreuses extensions contribuées par les utilisateurs.
HAUT DE PAGE4.3 Futur de Coq
Trente-deux ans après le premier prototype, la recherche autour de Coq est toujours aussi active, soutenue...
L'expertise technique et scientifique de référence
Cet article fait partie de l’offre
Technologies logicielles Architectures des systèmes
(240 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive
Évolution
BIBLIOGRAPHIE
-
(1) - * - The CompCert compiler. http://compcert.inria.fr.
-
(2) - * - OCaml page. http://www.ocaml.org/.
-
(3) - * - Page of the ACM Software System Award. http://awards.acm.org/software_system.
-
(4) - APPEL (A.W.), DOCKINS (R.), HOBOR (A.), BERINGER (L.), DODDS (J.), STEWART (G.), BLAZY (S.), LEROY (X.) - Program logics for certified compilers. - Cambridge University Press, 2014.
-
(5) - BARTHE (G.), GRÉGOIRE (B.), HERAUD (S.), ZANELLA-BÉGUELIN (S.) - - Computer-aided security proofs for the working cryptographer. In Advances in Cryptology – CRYPTO 2011, volume 6841 of Lecture Notes in Computer Science, pages 71–90. Springer, 2011.
-
(6) - BELNA (J.P.) - Histoire de la logique. - Ellipses, 2014.
- ...
DANS NOS BASES DOCUMENTAIRES
L'expertise technique et scientifique de référence
Cet article fait partie de l’offre
Technologies logicielles Architectures des systèmes
(240 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive
