Skip to Main content Skip to Navigation
Conference papers

On Teaching the Concept of Refinement with B

Abstract : The concept of refinement is central to the development of software. It appears in various forms in the different methodologies taught to students. A key point in the B method is the validation of the refinement step. The B methodology exhibits mathematical properties of correct refinements, and also automatically checkable conditions that ensure those properties. Some of the main pedagogical difficulties that the present authors found in teaching B centered around the notions linked to refinement, at the conceptual level, and at the tool level. Many papers have been published on the general benefits of the B method. This paper will focus on the specific concepts linked to refinements, and on the ones which need special care. We argue that, although B presents a complete mathematical analysis, it is beneficial to put the concept of refinement in perspective with other theories that come from formal methods, namely, in this paper, coalgebra and bisimulation.
Complete list of metadata

Cited literature [9 references]  Display  Hide  Download
Contributor : Evelyne Faivre Connect in order to contact the contributor
Submitted on : Wednesday, July 2, 2008 - 11:34:45 AM
Last modification on : Monday, December 14, 2020 - 12:28:43 PM
Long-term archiving on: : Friday, May 28, 2010 - 11:04:08 PM


Files produced by the author(s)


  • HAL Id : hal-00292648, version 1



Joanna Tomasik, Guy Vidal-Naquet. On Teaching the Concept of Refinement with B. Colloque The B Method from Research to Teaching., Jun 2008, Nantes, France. pp.109-120. ⟨hal-00292648⟩



Record views


Files downloads