Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

See discussions, stats, and author profiles for this publication at: https://ww

See discussions, stats, and author profiles for this publication at: https://www.researchgate.net/publication/47861673 Coq, un outil pour l'enseignement Article · January 2005 Source: OAI CITATIONS 2 READS 337 3 authors, including: Some of the authors of this publication are also working on these related projects: Relational Properties View project Automated Deduction View project David Delahaye Laboratoire d'Informatique, de Robotique et de Microélectronique de Montpellier… 50 PUBLICATIONS 547 CITATIONS SEE PROFILE Virgile Prevosto Atomic Energy and Alternative Energies Commission 57 PUBLICATIONS 1,199 CITATIONS SEE PROFILE All content following this page was uploaded by David Delahaye on 21 May 2014. The user has requested enhancement of the downloaded file. APPLICATION Coq, un outil pour l’enseignement Une expérience avec les étudiants du DESS Développement de logiciels sûrs David Delahaye* — Mathieu Jaume** — Virgile Prevosto*** * CPR – CEDRIC – CNAM 292, rue St Martin, F-75141 Paris Cedex 03, France David.Delahaye@cnam.fr ** SPI – LIP6 – Université Pierre et Marie Curie 8 Rue du Capitaine Scott, F-75015 Paris, France Mathieu.Jaume@lip6.fr *** Max-Planck Institut für Informatik Stuhlsatzenhausweg 85, D-66123 Saarbrücken, Allemagne INRIA Rocquencourt, BP 105, F-78153 Le Chesnay Cedex, France prevosto@mpi-inf.mpg.de, virgile.prevosto@inria.fr RÉSUMÉ. Cet article présente l’emploi de l’outil d’aide à la preuve Coq auprès d’étudiants de DESS (3e cycle universitaire). D’abord, dans le cadre d’un cours de sémantique des langages, Coq facilite l’appropriation par les étudiants de notions souvent jugées abstraites en leur per- mettant de les relier à des termes plus concrets. Ensuite, un projet informatique utilise Coq pour traiter des problèmes de plus grande envergure, faisant apparaître par là-même Coq comme un véritable outil de génie logiciel. Enﬁn, la réalisation de preuves dans l’atelier Focal a permis de fructueuses interactions avec le développement de ce système. ABSTRACT. In this article, we present the use of the Coq proof assistant with DESS (Master thesis) students. First, in the framework of a course of programming language semantics, Coq greatly helps the students to understand formal and abstract notions, such as induction, by binding them to more concrete terms. Next, a computer science project shows that Coq is also appropriate when dealing with larger problems. Last, we show how proofs developed by means of the Focal toolbox made it possible to get very valuable hints on the development of that system. MOTS-CLÉS : enseignement, sémantique, conception formelle, Coq, Focal. KEYWORDS: teaching, semantics of programming languages, formal conception, Coq, Focal. RSTI - TSI – 24/2005. Langages applicatifs, pages 1139 à 1160 1140 RSTI - TSI – 24/2005. Langages applicatifs 1. Introduction Dans cet article, nous présentons comment l’assistant à la preuve Coq a été uti- lisé, durant ces trois dernières années (de 2001 à 2004), comme outil d’enseignement auprès des étudiants du DESS DLS “Développement de Logiciels Sûrs” du CNAM et de l’université Pierre et Marie Curie. Le DESS DLS forme chaque année environ 25 étudiants aux métiers de la sûreté et de la sécurité des systèmes à logiciel pré- pondérant. Outre une formation classique (sémantique, analyse statique, temps réel, concurrence...), il vise à donner une formation aux méthodes formelles demandées dans les niveaux élevés de certiﬁcation (EAL 5-7, SIL 3-4) et aux outils associés : ate- lier B, Coq, outils de “model-checking”, Lustre/Esterel... Le public est principalement issu de maîtrise d’informatique. Les principales motivations pour l’utilisation de Coq dans nos activités d’ensei- gnement résident dans les difﬁcultés (et le manque de motivation !) qu’éprouvent certains étudiants en informatique vis à vis d’exercices de nature formelle. De plus, beaucoup d’étudiants ont l’habitude d’assimiler les enseignements au travers de tra- vaux pratiques et peu d’entre eux ont déjà une autonomie sufﬁsante pour la lecture de textes à caractère théorique. Le choix de Coq n’est pas primordial, les développe- ments présentés ici auraient sans doute pu être réalisés avec un autre système (pour une comparaison entre différents systèmes, on pourra, par exemple, consulter (Jakubiec et al., 1997; Grifﬁoen et al., 1998)). Coq (Coq Development Team, 2002) est un outil d’aide à la preuve ; il est actuelle- ment développé par le projet LogiCal à l’INRIA et au LRI (université d’Orsay). Il est basé sur la théorie des types (le calcul des constructions inductives pour être plus pré- cis) et utilise une logique de base intuitionniste. Les spéciﬁcations, les déﬁnitions, les théorèmes et les preuves formelles peuvent être réalisés de manière interactive et il est possible d’en extraire des programmes (isomorphisme de Curry-Howard). Les prin- cipales constructions de Coq utilisées en cours sont les types dépendants et les types inductifs. Ces derniers ressemblent aux types somme des langages fonctionnels, mais Coq engendre en outre automatiquement les principes d’induction correspondants. Par exemple, on peut déﬁnir les entiers de Peano à l’aide d’un type à deux contructeurs : Inductive peano_nat : Set := zero: peano_nat | succ: peano_nat -> peano_nat. Coq déﬁnit alors un terme peano_nat_ind, de type forall P:peano_nat->Prop, P zero -> (forall n:peano_nat, P n -> P (succ n)) -> forall n: peano_nat, P n Ce terme indique que si un prédicat P est vériﬁé par zero et si pour tout naturel n vériﬁant P, succ(n) vériﬁe P, alors P(n) est vrai pour tout n. Par ailleurs, P illustre la puissance des types dépendants. P déﬁnit en fait une fa- mille de types paramétrée par les termes de peano_nat. Ainsi on peut distinguer les termes (c’est à dire les preuves) de type P(zero), P(succ zero), etc. Coq, un outil pour l’enseignement 1141 L’emploi de Coq est décliné dans trois contextes différents. Coq est tout d’abord utilisé dans le cadre d’un cours d’introduction à la séman- tique des langages de programmation. Ce cours est souvent jugé difﬁcile par les étu- diants du fait de l’utilisation d’un formalisme mathématique permettant d’énoncer et de prouver des propriétés. Nous avons donc fait implanter dans Coq par les étudiants la quasi-totalité du cours de sémantique. Coq s’est révélé être un excellent vecteur de compréhension : implanter les notions étudiées permet de se les approprier en leur donnant forme et en pouvant les expérimenter. La section 2 présente les grandes lignes de ce cours de sémantique. Parallèlement, Coq a été, pour la première fois cette année (2003/2004), utilisé dans le cadre d’un projet. D’habitude, le projet est plutôt orienté programmation avec notamment l’utilisation d’OCaml (OCaml Development Team, 2004) (qui est présenté aux étudiants brièvement et de manière essentiellement pratique en début d’année sous la forme de cours de mise à niveau), mais même si elle se révèle plus subtile, l’acti- vité de preuve n’est pas fondamentalement différente de l’activité de programmation (au moins dans le système Coq où l’isomorphisme de Curry-Howard ne permet même plus de distinguer les deux activités). L’objectif de ce projet est de confronter les étu- diants à une application réelle (mais d’envergure raisonnable de manière à ne pas trop sous-spéciﬁer le problème) et non plus à des “exemples d’école” comme c’est volon- tairement le cas dans les quelques cours d’introduction à Coq dont les étudiants ont bénéﬁcié en début d’année (aﬁn qu’ils puissent, en particulier, commencer les preuves du cours de sémantique). Pour les étudiants, il est important de retirer de cet exemple réel la distinction entre raisonnement rigoureux et raisonnement formel. Notamment, il s’agit de bien comprendre le fossé existant entre une preuve mathématique (plus ou moins abstraite) et une preuve formelle (concrète et détaillée). Cet effort de concrétisa- tion aboutit généralement à des questions ﬁnalement très nouvelles pour ces étudiants “contraints”, par exemple, d’écrire des programmes qui terminent ou de choisir une représentation appropriée pour faciliter les preuves de correction. Le déroulement de ce projet est décrit en détail dans la section 3. Dans le cadre du cours de sémantique et du projet, les preuves demandées sont parfois longues et requièrent de temps à autre des récurrences un peu difﬁciles. En revanche, l’environnement dans lequel elles sont développées est complètement ex- plicité : les déﬁnitions et les propriétés s’ajoutent de manière incrémentale et toutes les preuves peuvent s’appuyer sur les résultats précédemment établis. Prouver des propriétés dans cette architecture “linéaire” correspond à une situation “idéale”. Le contexte de développement est parfois plus complexe. C’est notamment le cas lorsque l’on souhaite établir des propriétés dans le cadre d’une architecture hiérarchique (ap- proche objet, approche par rafﬁnements...). Aﬁn de sensibiliser les étudiants à ces problèmes, nous avons encadré des projets (associés au cours de conception formelle) consistant à utiliser l’atelier Focal (Prevosto et al., 2002a; Prevosto et al., 2002b; Focal development team, 2004; Prevosto, 2003). Il s’agit d’un atelier intégré de conception modulaire de logiciels certiﬁés. Chaque module de Focal peut être constitué d’un en- semble de déclarations, déﬁnitions, énoncés et preuves. On peut passer d’une spéciﬁ- 1142 RSTI - TSI – 24/2005. Langages applicatifs cation abstraite (ne contenant que des déclarations et des énoncés) à une implantation concrète (où tout est déﬁni et prouvé), à l’aide de mécanismes d’héritage et d’ins- tanciation de paramètres. Lors d’une étape d’héritage, des déclarations peuvent être rafﬁnées en déﬁnitions et des énoncés recevoir une preuve. En outre, une fonction déjà déﬁnie peut recevoir une nouvelle déﬁnition, plus efﬁcace dans le contexte du nouveau module. Le uploads/Ingenierie_Lourd/ coq-edu20tsi3904.pdf