Soundness Proof of EventB2Java. - Néstor Cataño; Shigeo Nishi (LADC, 2016)