W. V. Tran-Jørgensen, P. Automated Translation of VDM-SL to JML-Annotated Java. ECE-TR 2017, 5.