Generation of OCL constraints from B abstract machines

B is a formal method (and a specification language) which enables the automatic generation of an executable code through a succession of refinements stemming from an abstract specification. There are two current industrial tools (Clearsy's Atelier B-1, B-Core B Toolkit(2)) which provide support for all the development process (type-checking facilities, automatic and interactive proof support...). A B specification requires a certain knowledge of mathematical notations (Classical logic and sets) as well as specific terminology (generalized substitutions, B keywords) which may in all likelihood leave a non-specialist of the B notation in the dark. To address this problem, we will extract graphic elements from B specification in an effort to render it more understandable. In a previous work, these visual elements are illustrated in a UML class diagram. These visual elements being insufficient they are completed by OCL constraints allowing to present the invariant and the operations of a B abstract machine.