On Teaching the Concept of Refinement with B

Joanna Tomasik (1) , Guy Vidal-Naquet (1)

1 SUPELEC-Campus Gif

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.

Mots clés: Coalgebra; Gluing invariant; Morphism; Refinement

Domaines: Calcul formel [cs.SC]; Génie logiciel [cs.SE]

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⟩