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 metadatas

Cited literature [9 references]  Display  Hide  Download

https://hal-supelec.archives-ouvertes.fr/hal-00292648
Contributor : Evelyne Faivre <>
Submitted on : Wednesday, July 2, 2008 - 11:34:45 AM
Last modification on : Thursday, March 29, 2018 - 11:06:03 AM
Long-term archiving on: Friday, May 28, 2010 - 11:04:08 PM

File

JTOGVN-BDays2008-1.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00292648, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

207

Files downloads

93