Skip to Main content Skip to Navigation
Conference papers

Teaching programming methodology using Event B

Dominique Méry 1
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 metadatas
Contributor : Dominique Méry <>
Submitted on : Wednesday, June 11, 2008 - 12:21:02 PM
Last modification on : Friday, September 4, 2020 - 11:20:25 AM
Long-term archiving on: : Friday, September 28, 2012 - 3:50:27 PM


Files produced by the author(s)



Dominique Méry. Teaching programming methodology using Event B. The B method : from Research to Teaching, H. Habrias, Jun 2008, Nantes, France. ⟨10.1000/ISBN2-9512461-2-9⟩. ⟨inria-00287231v1⟩



Record views


Files downloads