Skip to main content
SpringerLink
Log in
Book cover

International Symposium of Formal Methods Europe

FME 1997: FME '97: Industrial Applications and Strengthened Foundations of Formal Methods pp 258–277Cite as

Automatic translation of VDM-SL specifications into gofer

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1313))

Abstract

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.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. B. K. Aichernig and P. G. Larsen. A Proof Obligation Generator for VDM-SL. Submitted to FME '97, 1997.

    Google Scholar 

  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. 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. H. Boehm and R. Cartwright. Exact Real Arithmetic. In D. Turner, editor, Research Topics in Functional Programming. Addison-Wesley, 1990.

    Google Scholar 

  5. P. Borba and S. Meira. From VDM Specifications to Functional Prototypes. Journal of Systems and Software, 21:267–278, 1993.

    Google Scholar 

  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. 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. N.E. Fuchs. Specifications are (preferably) executable. Software Engineering Journal, September 1992.

    Google Scholar 

  9. I.J. Hayes and C.B. Jones. Specifications are not (necessarily) executable. Software Engineering Journal, 4(6), 1989.

    Google Scholar 

  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. M. P. Jones. The implementation of the Gofer functional programming system. Technical Report YALE U/DCS/RR-1030, Yale University, 1994.

    Google Scholar 

  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. J. Launchbury and S. Peyton-Jones. Lazy Functional State Threads. In ACM Programming Languages Design and Implementation. ACM Press, 1993.

    Google Scholar 

  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. P. Mukherjee. Computer-aided Validation of Formal Specifications. Software Engineering Journal, 10(4):133–140, July 1995.

    Google Scholar 

  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. 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. G. O' Neill. Automatic Translation of VDM specifications into Standard ML programs. The Computer Journal, 35(6), 1992.

    Google Scholar 

  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. G. I. Parkin and G. O'Neill. Specification of the MAA standard in VDM. In Prehn and Toetenel [22].

    Google Scholar 

  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. 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 

Download references

Author information

Authors and Affiliations

  1. School of Computer Studies, University of Leeds, Leeds LS2 9JT, UK

    Paul Mukherjee

Authors
  1. Paul Mukherjee
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

John Fitzgerald Cliff B. Jones Peter Lucas

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mukherjee, P. (1997). Automatic translation of VDM-SL specifications into gofer. In: Fitzgerald, J., Jones, C.B., Lucas, P. (eds) FME '97: Industrial Applications and Strengthened Foundations of Formal Methods. FME 1997. Lecture Notes in Computer Science, vol 1313. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63533-5_14

Download citation

  • DOI: https://doi.org/10.1007/3-540-63533-5_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63533-8

  • Online ISBN: 978-3-540-69593-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation