Formal specifications using VDM