Automatic translation of VDM-SL specifications into gofer

  • Paul Mukherjee
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1313)


Interest in the use of functional languages for prototyping and animating formal specifications has decreased recently, as some of the limitations of traditional approaches have become apparent, in comparison to direct execution of the specification. In this paper we attempt to inject new life into this debate by describing how programs in a modern functional language may be automatically generated from formal specifications. We demonstrate how drawbacks of previous approaches are solved, and illustrate the success of the approach by describing errors found in published specifications.


State Transformer Record Type Functional Language Type Check Automatic Translation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    B. K. Aichernig and P. G. Larsen. A Proof Obligation Generator for VDM-SL. Submitted to FME '97, 1997.Google Scholar
  2. 2.
    V.S. Alagar, D. Muthiayen, and R. Achuthan. Animating Real-Time Reactive Systems. In A. Stoyenko, editor, ICECCS '96. IEEE Computer Society, 1995.Google Scholar
  3. 3.
    J.C. Bicarregui, J.S. Fitzgerald, P.A. Lindsay, R. Moore, and B. Ritchie. Proof in VDM: A Practitioner's Guide. Springer-Verlag, 1994.Google Scholar
  4. 4.
    H. Boehm and R. Cartwright. Exact Real Arithmetic. In D. Turner, editor, Research Topics in Functional Programming. Addison-Wesley, 1990.Google Scholar
  5. 5.
    P. Borba and S. Meira. From VDM Specifications to Functional Prototypes. Journal of Systems and Software, 21:267–278, 1993.Google Scholar
  6. 6.
    A. J. J. Dick, P. J. Krause, and J. Cozens. Computer Aided Transformation of Z into Prolog. In J. Nicholls, editor, Z User Workshop. Springer-Verlag, 1989.Google Scholar
  7. 7.
    R. Elmstrom, P.G. Larsen, and P.B. Lassen. The IFAD VDM-SL Toolbox: A Practical Approach to Formal Specifications. ACM Sigplan Notices, 29(9), 1994.Google Scholar
  8. 8.
    N.E. Fuchs. Specifications are (preferably) executable. Software Engineering Journal, September 1992.Google Scholar
  9. 9.
    I.J. Hayes and C.B. Jones. Specifications are not (necessarily) executable. Software Engineering Journal, 4(6), 1989.Google Scholar
  10. 10.
    P. Hudak, S.L. Peyton-Jones, and P. L. Wadler. Report on the Functional Programming Language Haskell: A Non-strict Purely Functional Language. ACM SIGPLAN Notices, 27(5), March 1992.Google Scholar
  11. 11.
    M. P. Jones. The implementation of the Gofer functional programming system. Technical Report YALE U/DCS/RR-1030, Yale University, 1994.Google Scholar
  12. 12.
    P.G. Larsen and P.B. Lassen. An Executable Subset of Meta-IV with Loose Specification. In Prehn and Toetenel [22].Google Scholar
  13. 13.
    J. Launchbury and S. Peyton-Jones. Lazy Functional State Threads. In ACM Programming Languages Design and Implementation. ACM Press, 1993.Google Scholar
  14. 14.
    D. MacQueen, R. Harper, and Milner R. Standard ML. Technical Report ECSLFCS-86-2, Department of Computer Science, University of Edinburgh, 1986.Google Scholar
  15. 15.
    P. Mukherjee. Computer-aided Validation of Formal Specifications. Software Engineering Journal, 10(4):133–140, July 1995.Google Scholar
  16. 16.
    P. Mukherjee and B.A. Wichmann. Formal Specification of the STV Algorithm. In M.G. Hinchey and J. P. Bowen, editors, Applications of Formal Methods. Prentice Hall, 1995.Google Scholar
  17. 17.
    D. S. Neilson and I. H. Sørenson. The B-Technologies: a system for computeraided programming. In 6th Nordic Workshop on Programming Theory, 1994.Google Scholar
  18. 18.
    G. O' Neill. Automatic Translation of VDM specifications into Standard ML programs. The Computer Journal, 35(6), 1992.Google Scholar
  19. 19.
    P. G. Larsen and B. S. Hansen and H. Brunn N. Plat and H. Toetenel and D. J. Andrews and J. Dawes and G. Parkin and others. Information technology-Programming languages, their environments and system software interfaces-Vienna Development Method-Specification Language-Part 1: Base language, December 1996.Google Scholar
  20. 20.
    G. I. Parkin and G. O'Neill. Specification of the MAA standard in VDM. In Prehn and Toetenel [22].Google Scholar
  21. 21.
    S. Peyton-Jones and P. Wadler. Imperative Functional Programming. In 20th ACM Symposium on Principles of Programming Languages. ACM Press, 1993.Google Scholar
  22. 22.
    S. Prehn and W. J. Toetenel, editors. VDM'91: Formal Software Development Methods, number 551 in Lecture Notes in Computer Science. Springer-Verlag, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Paul Mukherjee
    • 1
  1. 1.School of Computer StudiesUniversity of LeedsUK

Personalised recommendations