Skip to main content
SpringerLink
Log in

Program Specification and Verification in VDM

  • Conference paper
Logic of Programming and Calculi of Discrete Design

Part of the book series: NATO ASI Series ((NATO ASI F,volume 36))

Abstract

Formal methods employ mathematical notation in writing specifications and use mathematical reasoning in justifying designs with respect to such specifications. One avenue of formal methods research is known as the Vienna Development Method. VDM has been used on programming language and non-language applications. In this paper, programming languages and their compilers are ignored; the focus is on the specification and verification of programs.

VDM emphasizes the model-oriented approach to the specification of data. The reification of abstract objects to representations gives rise to proof obligations; one such set which has wide applicability assumes an increase in implementation bias during the design process. The incompleteness of this approach and an alternative set of rules are discussed.

The decision to show the input/output relation by post-conditions of two states is also a feature of VDM. In early publications, the proof obligations which support decomposition were poorly worked out; those presented below are as convenient to use as the original “Hoare-logic”. Recent work on a logic (which is tailored to partial functions) is also described.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. “Programming as a Mathematical Exercise”, J.R. Abrial, in “Mathematical Logic and Programming Languages”, (eds.) C.A.R. Hoare and J.C. Shepherdson, Prentice-Hall International, pp113–139, 1985.

    Google Scholar 

  2. “A Note on Program Verification”, P. Aczel, private communication, 1982.

    Google Scholar 

  3. “Program Construction and Verification”, R.C. Backhouse, Prentice-Hall International, 1986.

    Google Scholar 

  4. “A Logic Covering Undefinedness in Program Proofs”, H. Barringer, J.H. Cheng and C.B. Jones, Acta Informatica, Vol 21, No. 3, pp 251–269, 1984.

    Article  MathSciNet  MATH  Google Scholar 

  5. “Formal Specification and Software Development”, D. Bjorner and C.B. Jones, Prentice-Hall International, 1982.

    MATH  Google Scholar 

  6. “Partial Valued Logic”, S.R. Blarney, Ph.D. Thesis, Oxford University, 1980.

    Google Scholar 

  7. “A Verification Condition Generator for FORTRAN”, R.S. Boyer and J. Strother Moore, pp 9–101 in “The Correctness Problem in Computer Science”, (eds.) R.S. Boyer and J. Strother Moore, Academic Press, 1981.

    Google Scholar 

  8. “A Logic for Partial Functions”, J.H. Cheng, Ph.D Thesis, University of Manchester, 1986.

    Google Scholar 

  9. “On the Usability of Logics which Handle Partial Functions”, J.H. Cheng and C.B. Jones, forthcoming.

    Google Scholar 

  10. “The Munich Project CIP —Volume 1: The Wide Spectrum Language CIP-L”, CIP Language Group, Springer-Verlag, Lecture Notes in Computer Science, Vol.183, 1985.

    Google Scholar 

  11. “Implementing Mathematics with the Nuprl Proof Development System”, R.L. Constable, et al., Prentice-Hall, 1986.

    Google Scholar 

  12. “Project Support Environments for Formal Methods”, I.D. Cottam, C.B. Jones, T. Nipkow, A.C. Wills, M.I. Wolczko, A. Yaghi in “Integrated Project Support Environments”, (ed.) J. McDermid, Peter Peregrinus Ltd., 1985.

    Google Scholar 

  13. “Mule—An Environment for Rigorous Software Development”, I.D. Cottam, C.B. Jones, T.N. Nipkow, A.C. Wills, M. Wolczko and A. Yahgi, final Report to the SERC, June 1986.

    Google Scholar 

  14. “A Discipline of Programming”, E.W. Dijkstra, Series in Automatic Computation, Prentice-Hall, 1976.

    MATH  Google Scholar 

  15. “Edinburgh LCF”, M. Gordon, R. Milner and C. Wadsworth, Springer-Verlag, Lecture Notes in Computer Science, Vol.78, 1979.

    Book  MATH  Google Scholar 

  16. “The Science of Computer Programming”, D. Gries, Springer-Verlag, 1981.

    Google Scholar 

  17. “Data Refinement Refined”, H 3 .M.S 4, Oxford, Programming Research Group, draft typescript dated May 1985.

    Google Scholar 

  18. “An Introduction to Proving the Correctness of Programs”, S.L. Hantler and J.C. King, ACM Computing Surveys, Vol. 8, No. 3, pp 331–353, September 1976.

    Article  MathSciNet  MATH  Google Scholar 

  19. “Specification Case Studies”, I. Hayes, to be published by Prentice-Hall International, 1987.

    Google Scholar 

  20. “Data Refinement Refined: Resume”, J. He, C.A.R. Hoare and J.W. Sanders, ESOP ‘86, (eds.) B. Robinet and R. Wilhelm, Springer-Verlag, Lecture Notes in Computer Science, Vol. 213, 1986.

    Google Scholar 

  21. “Prespecification in Data Refinement”, J. He, C.A.R. Hoare and J.W. Sanders, submitted to Information Processing Letters, 1986.

    Google Scholar 

  22. “The Logic of Programming”, E.C.R. Hehner, Prentice-Hall International, 1984.

    Google Scholar 

  23. “An Axiomatic Basis for Computer Programming”, C.A.R. Hoare, CACM Vol.12, No.10, pp 576–580, October 1969.

    MATH  Google Scholar 

  24. “Proof of Correctness of Data Representations”, C.A.R. Hoare, Acta Informatica, Vol.1, pp 271–281, 1972.

    Article  MATH  Google Scholar 

  25. “Laws of Programming: A Tutorial Paper”, C.A.R. Hoare, He Jifeng, I.J. Hayes, C.C. Morgan, J.W. Sanders, I.H. Sorensen, J.M. Spivey, B.A. Sufrin and A.W. Roscoe, Oxford University Technical Monograph, PRG-45, May 1985.

    Google Scholar 

  26. “A Technique for Showing that Two Functions Preserve a Relation between their Domains”, C.B. Jones, IBM Laboratory, Vienna, LR 25.3.067, April, 1970.

    Google Scholar 

  27. “Formal Development of Correct Algorithms: An Example Based on Earley’s Recogniser”, C.B. Jones, Proceedings of the 1972 Las Cruces Conference, SIGPLAN Notes, Vol. 7, No.l, 1972. (Full version published as IBM Technical Report TR 12.095, IBM U.K. Laboratories, Hursley, December 1971.)

    Google Scholar 

  28. “Formal Definition in Compiler Development”, C.B. Jones, IBM Laboratory Vienna, TR 25.145, February 1976.

    Google Scholar 

  29. “Implementation Bias in Constructive Specifications of Abstract Objects”, C.B. Jones, 1977.

    Google Scholar 

  30. “Software Development: A Rigorous Approach”, C.B. Jones, Prentice-Hall International, 1980.

    MATH  Google Scholar 

  31. “Development Methods for Computer Programs including a Notion of Interference”, C.B. Jones, Oxford University, PRG-25, June 1981.

    Google Scholar 

  32. “Systematic Program Development”, C.B. Jones, in “Mathematics and Computer Science”, (eds.) J.W. de Bakker, M. Hazewinkel and J.K. Lenstra, CWI Monographs, North Holland Publishers, pp 19–50, 1986.

    Google Scholar 

  33. “Systematic Software Development using VDM”, C.B. Jones, Prentice-Hall International, 1986.

    MATH  Google Scholar 

  34. “Teaching Notes for Systematic Software Development using VDM”, C.B. Jones, Department of Computer Science Technical Report, UMCS-86–4–2, Manchester University, 1986.

    Google Scholar 

  35. “Some Requirements for Formal Reasoning Support”, C.B. Jones and C.P. Wadsworth, forthcoming.

    Google Scholar 

  36. “Sorting and Searching”, D.E. Knuth, in The Art of Computer Programming’, Vol. III, Addison-Wesley Publishing Company, 1975.

    Google Scholar 

  37. “Sequent Calculus and Partial Logic”, G. Koletsos, M.Sc. Thesis, Manchester University, 1976.

    Google Scholar 

  38. “Abstraction and Specification in Program Development”, B. Liskov and J. Guttag, MIT Press, 1986.

    MATH  Google Scholar 

  39. “Two Constructive Realizations of the Block Concept and their Equivalence”, P. Lucas, IBM Laboratory Vienna, Technical Report TR 25.085, June, 1968.

    Google Scholar 

  40. “On The Formal Description of PL/I”, P. Lucas and K. Walk, Annual Review in Automatic Programming, Vol. 6, Part 3, Pergamon Press, 1969.

    Google Scholar 

  41. “A Basis for a Mathematical Theory for Computation”, J. McCarthy, in “Computer Programming and Formal Systems”, (eds.) P. Braffort and D. Hirschberg, North-Holland Publishing Company, pp 33–70, 1967.

    Google Scholar 

  42. “A Formal Specification of Straight Lines on Graphic Devices”, Lynn S. Marshall, (in) “Formal Methods and Software Development”, Proceedings of the Int. Joint Conference on Theory and Practice of Software Development (TAPSOFT), Berlin, Vol 2: Colloquium on Software Engineering, Springer Verlag, Lecture Notes in Computer Science, Vol. 186, pp 129–147, March, 1985.

    Chapter  Google Scholar 

  43. “An Early Program Proof by Alan Turing”, F.L. Morris and C.B. Jones, “Annals of the History of Computing”, Vol.6 No.2, pp l39–143, April, 1984.

    Google Scholar 

  44. “Non-Deterministic Data Types: Models and Implementations”, T. Nipkow, Internal Report, University of Manchester, June 1985.

    Google Scholar 

  45. “Non-Deterministic Data Types: Models and Implementations”, T. Nipkow, Springer-Verlag, Acta Informatica Vol. 22, pp 629–661, 1986.

    Article  MathSciNet  MATH  Google Scholar 

  46. “An Approach to Program Reasoning Based on a First Order Logic for Partial Functions”, O. Owe, privately circulated, June 1984 .

    Google Scholar 

  47. “Partial Function Logic”, G. D. Plotkin, Lectures at Edinburgh University, 1985.

    Google Scholar 

  48. “Existence and Description in Formal Logic”, in “Bertrand Russell, Philosopher of the Century”, (ed.), Schoemann, Allen and Unwin, 1967.

    Google Scholar 

  49. “A Language of Specified Programs”, A. Tarlecki.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Manchester University, M13 9PL, UK

    C. B. Jones

Authors
  1. C. B. Jones
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Fakultät für Mathematik und Informatik, Universität Passau, Postfach 2540, 8390, Passau, Federal Republic of Germany

    Manfred Broy

Rights and permissions

Reprints and permissions

Copyright information

© 1987 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Jones, C.B. (1987). Program Specification and Verification in VDM. In: Broy, M. (eds) Logic of Programming and Calculi of Discrete Design. NATO ASI Series, vol 36. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-87374-4_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-87374-4_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-87376-8

  • Online ISBN: 978-3-642-87374-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation