Within the design process, a high-level specification is subject to two conflicting tensions. It is used as a vehicle for validating the requirements, and also as a first step of the refinement process. Whilst the structuring mechanisms available in the B method are well-suited for the latter purpose, the rich type constructions of VDM are useful for the former.

In this paper we propose a method which synthesises a structured B design from a flat VDM specification by analysing how type definitions are used within the VDM state in order to generate a corresponding B machine hierarchy.