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 metadatas

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/inria-00287231
Contributor : Dominique Méry <>
Submitted on : Thursday, November 13, 2008 - 12:13:34 AM
Last modification on : Thursday, September 19, 2019 - 5:00:14 PM
Long-term archiving on : Saturday, November 26, 2016 - 2:39:49 AM

File

entcsmery.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00287231, version 2

Collections

Citation

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

Share

Metrics

Record views

168

Files downloads

239