Skip to Main content Skip to Navigation
New interface
Conference papers

Teaching programming methodology using Event B

Dominique Méry 1, * 
* Corresponding author
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download
Contributor : Dominique Méry Connect in order to contact the contributor
Submitted on : Thursday, November 13, 2008 - 12:13:34 AM
Last modification on : Friday, February 4, 2022 - 3:22:34 AM
Long-term archiving on: : Saturday, November 26, 2016 - 2:39:49 AM


Files produced by the author(s)


  • HAL Id : inria-00287231, version 2



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



Record views


Files downloads