The B method as an environment for the verification of eiffel programs: a case study

Abstract

In this paper we present an attempt to represent Eiffel programs as B specifications. Our purpose is to use the B method as an environment for the verification of the correctness of Eiffel programs. We study the difficulties associated with the representation of object oriented features (inherent to Eiffel programs) in the non object oriented B language. We use an extension to B in order to represent dynamic creation and deletion of objects, and show how object interaction can be achieved by borrowing some ideas from software architectures. The paper is centred on a simple and well known case study, the tra- ditional object oriented implementation of generic lists.