Présentation

Article

1 - EXEMPLE DE DÉVELOPPEMENT EN COQ : PREUVE DE CORRECTION D’UN ALGORITHME SIMPLE

  • 1.1 - Établissement d’un contexte de travail
  • 1.2 - Définition du tri par insertion
  • 1.3 - Spécification de la fonction sort
  • 1.4 - Preuve interactive de correction de sort
  • 1.5 - Après la preuve
  • 1.6 - Extraction de programmes

2 - APPLICATIONS PRINCIPALES

  • 2.1 - Utilité pour la programmation impérative
  • 2.2 - Informatique fondamentale et mathématiques

3 - COQ ET SA PLACE EN INFORMATIQUE

4 - ÉVOLUTION

  • 4.1 - Outil issu de la recherche fondamentale
  • 4.2 - Outil actuel
  • 4.3 - Futur de Coq

5 - APPRENDRE COQ

6 - CONCLUSION

Article de référence | Réf : H3310 v1

Conclusion
Coq, assistant de preuve

Auteur(s) : Sandrine Blazy, Pierre Castéran, Hugo Herbelin

Date de publication : 10 août 2017

Pour explorer cet article
Télécharger l'extrait gratuit

Vous êtes déjà abonné ?Connectez-vous !

Sommaire

Présentation

Version en anglais 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’article

Auteur(s)

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.

Cet article est réservé aux abonnés.
Il vous reste 92% à découvrir.

Pour explorer cet article
Téléchargez l'extrait gratuit

Vous êtes déjà abonné ?Connectez-vous !


L'expertise technique et scientifique de référence

La plus importante ressource documentaire technique et scientifique en langue française, avec + de 1 200 auteurs et 100 conseillers scientifiques.
+ de 10 000 articles et 1 000 fiches pratiques opérationnelles, + de 800 articles nouveaux ou mis à jours chaque année.
De la conception au prototypage, jusqu'à l'industrialisation, la référence pour sécuriser le développement de vos projets industriels.

DOI (Digital Object Identifier)

https://doi.org/10.51257/a-v1-h3310


Cet article fait partie de l’offre

Technologies logicielles Architectures des systèmes

(239 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

ABONNEZ-VOUS

Version en anglais English

6. Conclusion

Les assistants de preuve tels que Coq rendent possible la production de logiciels sûrs malgré leur complexité. Il est bien clair que tout programme ne doit pas être formellement vérifié, mais le nombre d’applications devant être sûres justifie l’émergence d’un métier que nous pouvons appeler ingénierie de la preuve, qui nécessite des compétences à la fois en logique et en génie logiciel.

Parmi les divers assistants de preuve, Coq se distingue par sa fiabilité, une bibliothèque standard très fournie, et un grand nombre de tactiques de preuve interactive.

Sa complexité pourrait effrayer l’utilisateur novice, mais on peut remarquer que ce n’est pas Coq qui est trop compliqué, mais la preuve rigoureuse, notamment d’algorithmes et de programmes, qui nécessite des outils suffisamment complets.

HAUT DE PAGE

Cet article est réservé aux abonnés.
Il vous reste 93% à découvrir.

Pour explorer cet article
Téléchargez l'extrait gratuit

Vous êtes déjà abonné ?Connectez-vous !


L'expertise technique et scientifique de référence

La plus importante ressource documentaire technique et scientifique en langue française, avec + de 1 200 auteurs et 100 conseillers scientifiques.
+ de 10 000 articles et 1 000 fiches pratiques opérationnelles, + de 800 articles nouveaux ou mis à jours chaque année.
De la conception au prototypage, jusqu'à l'industrialisation, la référence pour sécuriser le développement de vos projets industriels.

Cet article fait partie de l’offre

Technologies logicielles Architectures des systèmes

(239 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

ABONNEZ-VOUS

Lecture en cours
Conclusion
Sommaire
Sommaire

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

Cet article est réservé aux abonnés.
Il vous reste 93% à découvrir.

Pour explorer cet article
Téléchargez l'extrait gratuit

Vous êtes déjà abonné ?Connectez-vous !


L'expertise technique et scientifique de référence

La plus importante ressource documentaire technique et scientifique en langue française, avec + de 1 200 auteurs et 100 conseillers scientifiques.
+ de 10 000 articles et 1 000 fiches pratiques opérationnelles, + de 800 articles nouveaux ou mis à jours chaque année.
De la conception au prototypage, jusqu'à l'industrialisation, la référence pour sécuriser le développement de vos projets industriels.

Cet article fait partie de l’offre

Technologies logicielles Architectures des systèmes

(239 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

ABONNEZ-VOUS