  We present a machine-checked soundness proof of a translation of Event-B to
the Java Modeling Language (JML). The translation is based on an operator
EventB2Jml that maps Evnet-B events to JML method specifications, and
deterministic and non-deterministic assignments to JML method post-conditions.
This translation has previously been implemented as the EventB2Jml tool. We
adopted a taking our own medicine approach in the formalisation of our proof so
that Event-B as well as JML are formalised in Event-B and the proof is
discharged with the Rodin platform. Hence, for any Event-B substitution
(whether an event or an assignment) and for the JML method specification
obtained by applying EventB2Jml to the substitution, we prove that the
semantics of the JML method specification is simulated by the semantics of the
substitution. Therefore, the JML specification obtained as translation from the
Event-B substitution is a refinement of the substitution. Our proof includes
invariants and the standard Event-B initialising event, but it does not include
full machines or Event-B contexts. We assume that the semantics of JML and
Event-B operate both on the same initial and final states, and we justify our
assumption.
