Abstract
In the continuity of our research on integration of UML and B, we address in this paper the transformation from OCL (Object Constraint Language), which is an integral part of UML, into B. Our derivation schemes allow to systematically even automatically derive into B not only the complementary class invariants, the state-chart guard conditions, but also the OCL specification for UML operations.