Teaching programming methodology using Event B

Dominique Méry 1, *
* Auteur correspondant
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Event B is supported by the RODIN platform and provides a framework for teaching programming methodology based on the famous pre/post specifications, together with the refinement. We illustrate a methodology based on Event B and the refinement by developing Floyd's algorithm for computing the shortest distances of a graph, which is based on an algorithm design technique called dynamic programming. The development is based on a paradigm identifying a non-deterministic event with a procedure call and by introducing control states. We discuss points related to our lectures at the university.
Type de document :
Communication dans un congrès
Henri Habrias. The B Method: from Research to Teaching, Jul 2008, Nantes, France. APCB, 2008
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00287231
Contributeur : Dominique Méry <>
Soumis le : jeudi 13 novembre 2008 - 00:13:34
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52
Document(s) archivé(s) le : samedi 26 novembre 2016 - 02:39:49

Fichier

entcsmery.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00287231, version 2

Collections

Citation

Dominique Méry. Teaching programming methodology using Event B. Henri Habrias. The B Method: from Research to Teaching, Jul 2008, Nantes, France. APCB, 2008. 〈inria-00287231v2〉

Partager

Métriques

Consultations de la notice

156

Téléchargements de fichiers

124