Skip to main content
SpringerLink
Log in

The Typed Logic of Partial Functions and the Vienna Development Method

  • Chapter
  • First Online:
Logics of Specification Languages

Abstract

Decisions about the logic underpinning a formal specification language have important consequences for the utility of the formalism. This chapter describes the major features of the typed Logic of Partial Functions (LPF) as it has been implemented in support of the Vienna Development Method’s Specification Language, VDM-SL. It compares attempts to realise the logic in different environments: a usercentred proof support tool, a specification interpreter and an automated proof tool. Future directions in integrated proof support for the language are suggested.

For Harry Fitzgerald, Engineer (1928–2004)

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 129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 169.99
Price excludes VAT (USA)
  • Durable hardcover 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. S. Agerholm. Translating specifications in VDM-SL to PVS. In J. von Wright, J. Grundy, and J. Harrison, editors, Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics (TPHOLs’96), volume 1125 of Lecture Notes in Computer Science, pages 1–16. Springer, 1996.

    Google Scholar 

  2. S. Agerholm, J. Bicarregui, and S. Maharaj. On the Verification of VDM Specifications and Refinement with PVS. In J.C. Bicarregui, editor, Proof in VDM: Case Studies, FACIT. Springer, 1998.

    Google Scholar 

  3. S. Agerholm and J. Frost. Towards an Integrated CASE and Theorem Proving Tool for VDM-SL. In J.S. Fitzgerald, C.B. Jones, and P. Lucas, editors, FME’97: Industrial Applications and Strengthened Foundations of Formal Methods (Proceedings of the 4th Internatinal Symposium of Formal Methods Europe, Graz, Austria, September 1997), volume 1313 of Lecture Notes in Computer Science, pages 278–297. Springer, 1997.

    Google Scholar 

  4. S. Agerholm and J. Frost. Supporting Proof in VDM-SL using Isabelle. In J.C. Bicarregui, editor, Proof in VDM: Case Studies, FACIT. Springer, 1998.

    Google Scholar 

  5. S. Agerholm and P.G. Larsen. A Lightweight Approach to Formal Methods. In Proceedings of the International Workshop on Current Trends in Applied Formal Methods, Boppard, Germany, Springer, 1998.

    Google Scholar 

  6. M. Mac an Airchinnigh. Tutorial Lecture Notes on the Irish School of the VDM. In S. Prehn and W.J. Toetenel, editors, VDM’91-Formal Software Development Methods, volume 552 of Lecture Notes in Computer Science, pages 141–237. Springer, October 1991.

    Google Scholar 

  7. D.J. Andrews, editor. Information Technology-Programming Languages, Their Environments and System Software Interfaces: Vienna Development Method-Specification Language-Part 1: Base Language. International Organization for Standardization, December 1996. International Standard ISO/IEC 13817-1.

    Google Scholar 

  8. M. Barnett, R. DeLine, B. Jacobs, M. Fähndrich, K. R. M. Leino, W. Schulte, and H. Venter. The Spec# Programming System: Challenges and Directions. In Proceedings of the International Conference on Verified Software: Theories, Tools, Experiments, 2005. http://vstte.ethz.ch/papers.html.

    Google Scholar 

  9. H. Barringer, J.H. Cheng, and C.B. Jones. A Logic Covering Undefinedness in Program Proofs. Acta Informatica, 21:251–269, 1984.

    Article  MathSciNet  Google Scholar 

  10. J. C. Bicarregui, J. S. Fitzgerald, P. A. Lindsay, R. Moore, and B. Ritchie. Proof in VDM: A Practitioner’s Guide, FACIT. Springer, 1994.

    Google Scholar 

  11. J.C. Bicarregui, D. MacRandal, B. Matthews, and B. Ritchie. Return to the Theorem Prover’s House: Application of the Learning Grid to Formal Methods. In S. Curtis and M. Green, editors, Proceedings of the Workshop on Teaching Formal Methods: Practice and Experience, pages 82–90, December 2003. http://cms.brookes.ac.uk/tfm2003/.

    Google Scholar 

  12. D. Bjørner and C. B. Jones, editors. Formal Specification and Software Development. Prentice-Hall International, 1982.

    Google Scholar 

  13. R. Bloomfield and P. Froome. The Application of Formal Methods to the Assesment of High Integrity Software. IEEE Transactions on Software Engineering, SE-12(9):988–993, September 1986.

    Article  Google Scholar 

  14. R. Bloomfield, P. Froome, and B. Monahan. SpecBox: A Toolkit for BSI-VDM. SafetyNet, 5:4–7, 1989.

    Google Scholar 

  15. P. Chalin. Logical Foundations of Program Assertions: What do Practitioners Want? In Bernhard K. Aichernig and Bernhard Beckert, editors, Proceedings of the 3rd International Conference on Software Engineering and Formal Methods (SEFM’05), pages 383–393. IEEE Computer Society Press, September 2005.

    Google Scholar 

  16. J.H. Cheng. A Logic for Partial Functions. PhD thesis, Department of Computer Science, University of Manchester, 1986. UMCS-86-7-1.

    Google Scholar 

  17. J.H. Cheng and C.B. Jones. On the Usability of Logics Which Handle Partial Functions. In C. Morgan and J. Woodcock, editors, Proceedings of the Third Refinement Workshop. Springer, 1990.

    Google Scholar 

  18. L. A. Dennis, G. Collins, M. Norrish, R. Boulton, K. Slind, G. Robinson, M. Gordon, and T. Melham. The PROSPER Toolkit. In Proceedings of the 6th Inter-national Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 1785 of Lecture Notes in Computer Science. Springer, 2000.

    Google Scholar 

  19. E.H. Döurr and N. Plat (editors). VDM++ Language Reference Manual. Afrodite (ESPRIT-III project number 6500), Cap Volmac, August 1995.

    Google Scholar 

  20. J. S. Fitzgerald. Modularity in Model-Oriented Formal Specifications and its Interaction with Formal Reasoning. PhD thesis, Department of Computer Science, University of Manchester, November 1991. Technical Report UMCS-91-11-2.

    Google Scholar 

  21. J. S. Fitzgerald and C. B. Jones. Proof in the Analysis of a Model of a Tracking System. In J.C. Bicarregui, editor, Proof in VDM: Case Studies, Formal Approaches to Computing and Information Technology, pages 1–29. Springer, 1998.

    Google Scholar 

  22. J. S. Fitzgerald and P. G. Larsen. Modelling Systems-Practical Tools and Techniques in Software Development. Cambridge University Press, 1998.

    Google Scholar 

  23. J. S. Fitzgerald, P. G. Larsen, P. Mukherjee, N. Plat, and M. Verhoef. Validated Designs for Object-oriented Systems. Springer, London, 2005. ISBN 1-85233-881-4.

    MATH  Google Scholar 

  24. J. S. Fitzgerald, P. G. Larsen, and N. Plat, editors. Towards Next Generation Tools for VDM: Contributions to the First International Overture Workshop, Newcastle, July 2005. Technical Report CS-TR-969, School of Computing Science, Newcastle University, June 2006.

    Google Scholar 

  25. J. S. Fitzgerald and R. Moore. Experiences in Developing a Proof Theory for VDM Specifications. In D. J. Andrews, J. F. Groote, and C. A. Middelburg, editors, Proceedings of the International Workshop on Semantics of Specification Languages. Springer, 1994.

    Google Scholar 

  26. W. Henhapl and C.B. Jones. The Block Concept and Some Possible Implementations, with Proofs of Equivalence. Technical Report 25.104, IBM Laboratory, Vienna, April 1970.

    Google Scholar 

  27. J. Hörl and B. K. Aichernig. Validating Voice Communication Requirements Using Lightweight Formal Methods. IEEE Software, May 2000.

    Google Scholar 

  28. D. Jackson and J. Wing. Lightweight Formal Methods. IEEE Computer, 29(4):22–23, April 1996.

    Google Scholar 

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

    Google Scholar 

  30. C. B. Jones. Systematic Software Development Using VDM. Prentice-Hall International, 1986.

    Google Scholar 

  31. C. B. Jones. Systematic Software Development Using VDM, 2nd edition. Prentice-Hall International, 1990.

    Google Scholar 

  32. C. B. Jones. A Rigorous Approach to Formal Methods. IEEE Computer, 29(4):20–21, April 1996.

    Article  MathSciNet  Google Scholar 

  33. C. B. Jones. Scientific Decisions which Characterize VDM. In J.M. Wing, J.C.P. Woodcock, and J. Davies, editors, FM’99: Formal Methods, volume 1708 of Lecture Notes in Computer Science, pages 28–47. Springer, 1999.

    Google Scholar 

  34. C. B. Jones. Reasoning About Partial Functions in the Formal Development of Programs. Electronic Notes in Theoretical Computer Science, 145:3–25, January 2006.

    Article  Google Scholar 

  35. C. B. Jones and P. Lucas. Proving correctness of Implementation Techniques. In E. Engeler, editor, A Symposium on Algorithmic Languages, volume 188 of Lecture Notes in Computer Science, pages 178–211. Springer, 1971.

    Google Scholar 

  36. C. B. Jones and C. A. Middelburg. A Typed Logic of Partial Functions Reconstructed Classically. Acta Informatica, 31(5):399–430, 1994.

    Article  MathSciNet  Google Scholar 

  37. C.B. Jones, K.D. Jones, P.A. Lindsay, and R. Moore, editors. mural: A Formal Development Support System. Springer, 1991.

    Google Scholar 

  38. J. R. Kiniry, P. Chalin, and C. Hurlin. Integrating Static Checking and Interactive Verification: Supporting Multiple Theories and Provers in Verification. In Proceedings of the International Conference on Verified Software: Theories, Tools, Experiments, 2005. http://vstte.ethz.ch/papers.html.

    Google Scholar 

  39. P. G. Larsen. Towards Proof Rules for VDM-SL. PhD thesis, Technical University of Denmark, Department of Computer Science, March 1995. ID-TR:1995-160.

    Google Scholar 

  40. P. G. Larsen, J. S. Fitzgerald, and T. Brookes. Applying Formal Specification in Industry. IEEE Software, 13(3):48–56, May 1996.

    Article  Google Scholar 

  41. P. G. Larsen and B. S. Hansen. Semantics for underdetermined expressions. Formal Aspects of Computing, 8(1):47–66, January 1996.

    Article  Google Scholar 

  42. P. G. Larsen and P. B. Lassen. An Executable Subset of Meta-IV with Loose Specification. In VDM’ 91: Formal Software Development Methods. VDM Europe, Springer, 1991.

    Google Scholar 

  43. P. Lucas. Two constructive realizations of the block concept and their equivalence. Technical Report 25.085, IBM Laboratory, Vienna, 1968.

    Google Scholar 

  44. P. Lucas. Note on strong meaning of logical operators. Technical Report 25.3.051, IBM Laboratory, Vienna, 1969.

    Google Scholar 

  45. P. Lucas and K. Walk. On the formal description of PL/I. Annual Review of Automatic Programming Part 3, 6(3), 1969.

    Google Scholar 

  46. Z. Manna and J. McCarthy. Properties of Programs and Partial Function Logic. In B. Meltzer and D. Michie, editors, Machine Intelligence 5, pages 27–37. Edinburgh University Press, 1969.

    Google Scholar 

  47. J. McCarthy. A Basis for a Mathematical Theory of Computation. In P. Braffort and D. Hirschberg, editors, Computer Programming and Formal Systems, pages 33–70. North-Holland, 1967.

    Google Scholar 

  48. P. Mukherjee. Computer-aided Validation of Formal Specifications. Software Engineering Journal, pages 133–140, July 1995.

    Google Scholar 

  49. The RAISE Language Group. The RAISE Specification Language. The BCS Practitioner Series. Prentice Hall, 1992.

    Google Scholar 

  50. The RAISE Language Group. The RAISE Development Method. The BCS Practitioner Series. Prentice Hall, 1995.

    Google Scholar 

  51. M. Verhoef, P. G. Larsen, and J. Hooman. Modeling and Validating Distributed Embedded Real-Time Systems with VDM++. In J. Misra and T. Nipkow, editors, FM 2006, volume 4085 of Lecture Notes in Computer Science. Springer, 2006. To appear.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Centre for Software Reliability, Newcastle University, Newcastle upon Tyne, NE1 7RU, UK

    John S. Fitzgerald

Authors
  1. John S. Fitzgerald
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Informatics and Mathematical Modelling, Technical University of Denmark, 2800, Kgs. Lyngby, Denmark

    Dines Bjørner

  2. Department of Computer Science, University of Essex, Wivenhoe Park, CO4 3SQ, Colchester, UK

    Martin C. Henson

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Fitzgerald, J.S. (2008). The Typed Logic of Partial Functions and the Vienna Development Method. In: Bjørner, D., Henson, M.C. (eds) Logics of Specification Languages. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74107-7_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-74107-7_9

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-74106-0

  • Online ISBN: 978-3-540-74107-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation