Coq, un outil pour l'enseignement. Une expérience avec les étudiants du DESS Développement de logiciels sûrs
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.
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.
D.DELAHAYE, M.JAUME, V.PREVOSTO
enseignement, sémantique, conception formelle, Coq, Focal.
teaching, semantics of programming languages, formal conception, Coq, Focal.
Français
|
