In this work, we present a translation from B machines to JML specifications. Our work allows developers to use different formal methods techniques and tools at different software development phases. A developer can use B's strong support for model verification during early stages of software development to produce a fully verified model of the application, and then transition to JML to simplify the task of producing a Java implementation and to take advantage of JML (semi-) automatic tools such as runtime assertion checkers. We have validated our implementation of the translation by applying it to a moderately complex B model of a social networking site, and then by executing the resulting JML specifications against a suite of test cases developed for a hand-translation of the B model. We have implemented the translation as the B2Jml tool, which has been integrated to the ABTools suite.