A System for Translating Executable VDM Specifications into Lazy ML

This article describes the process of developing a system for translating VDM executable specifications into Lazy ML prototypes. The system was specified in VDM and a Lazy ML prototype implementation was derived from its specification. This article concentrates on discussing the lessons learned in each stage of the development process, evaluating the adequacy of the used methodology. © 1997 by John Wiley & Sons, Ltd.