On Teaching the Concept of Refinement with B
https://www.academia.edu/13917699/On_Teaching_the_Concept_of_Refinement_with_B?email_work_card=abstract-read-more Joanna Tomasik Guy Vidal-Naquet Computer Science Department SUPELEC Gif-sur-Yvette, France 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, althoug...