ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne
Autres revues >>

Technique et Science Informatiques

0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 24/9 - 2005  - pp.1139-1160  - doi:10.3166/tsi.24.1139-1160
TITRE
Coq, un outil pour l'enseignement. Une expérience avec les étudiants du DESS Développement de logiciels sûrs

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 permettant 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. Enfin, 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.


AUTEUR(S)
David DELAHAYE, Mathieu JAUME, Virgile PREVOSTO

MOTS-CLÉS
enseignement, sémantique, conception formelle, Coq, Focal.

KEYWORDS
teaching, semantics of programming languages, formal conception, Coq, Focal.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 12.5 €
• Non abonné : 25.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (348 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier