Skip to main content
SpringerLink
Log in

Proof Obligation Generation and Discharging for Recursive Definitions in VDM

  • Conference paper
Formal Methods and Software Engineering (ICFEM 2010)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6447))

Included in the following conference series:

Abstract

A proof obligation is a theorem stating that a certain property must hold in order for a formal specification to be internally consistent. If a proof obligation can be proved, then the referred part in the specification is consistent. The generation of proof obligations to check for a specification’s internal consistency is a concept that has been applicable in a VDM context for a long time. This work is extending the existing proof obligation generation capabilities with proof obligations for the termination of recursive functions. Those proof obligations can then automatically be moved over to HOL and the corresponding proofs can be carried out in that framework. Depending upon the nature of the recursion, the discharge of these proofs can be done automatically. This paper will categorise the different kinds of recursion.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. Aichernig, B.K., Larsen, P.G.: A Proof Obligation Generator for VDM-SL. In: Fitzgerald, J.S., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol. 1313, pp. 3–540. Springer, Heidelberg (1997) ISBN 3-540-63533-5

    Google Scholar 

  2. Owre, S., Rushby, J.M., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)

    Google Scholar 

  3. Ribeiro, A.: An Extended Proof Obligation Generator for VDM++/OML. Master’s thesis, Minho University with exchange to Engineering College of Arhus (July 2008)

    Google Scholar 

  4. Vermolen, S.: Automatically Discharging VDM Proof Obligations using HOL. Master’s thesis, Radboud University Nijmegen, Computer Science Department (August 2007)

    Google Scholar 

  5. Vermolen, S., Hooman, J., Larsen, P.G.: Automating Consistency Proofs of VDM++ Models using HOL. In: Proceedings of the 25th Symposium On Applied Computing (SAC 2010), Sierre, Switzerland. ACM Press, New York (March 2010)

    Google Scholar 

  6. Gordon, M.: HOL: A Proof Generating System for Higher-Order Logic. In: Birtwistle, G., Subrahmanyam, P.A. (eds.) VLSI Specification, Verification, and Synthesis, Kluwer Academic Publishers, Dordrecht (1987)

    Google Scholar 

  7. Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, London (1979)

    MATH  Google Scholar 

  8. Fitzgerald, J., Larsen, P.G., Mukherjee, P., Plat, N., Verhoef, M.: Validated Designs for Object–oriented Systems. Springer, New York (2005)

    MATH  Google Scholar 

  9. Fitzgerald, J., Larsen, P.G.: Modelling Systems – Practical Tools and Techniques in Software Development. Cambridge University Press, Cambridge (1998) ISBN 0-521-62348-0

    MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  11. McCarthy, J.: A Basis for a Mathematical Theory of Computation. In: Braffort, P., Hirstberg, D. (eds.) Western Joint Computer Conference. Then published in: Computer Programming and Formal Systems, pp. 33–70. North Holland, Amsterdam (1961)

    Google Scholar 

  12. Elmstrøm, R., Larsen, P.G., Lassen, P.B.: The IFAD VDM-SL Toolbox: A Practical Approach to Formal Specifications. ACM Sigplan Notices 29(9), 77–80 (1994)

    Article  Google Scholar 

  13. Fitzgerald, J., Larsen, P.G., Sahara, S.: VDMTools: Advances in Support for Formal Modeling in VDM. Sigplan Notices 43(2), 3–11 (2008)

    Article  Google Scholar 

  14. Larsen, P.G., Battle, N., Ferreira, M., Fitzgerald, J., Lausdahl, K., Verhoef, M.: The Overture Initiative – Integrating Tools for VDM. ACM Software Engineering Notes 35(1) (January 2010)

    Google Scholar 

  15. Aichernig, B.: A Proof Obligation Generator for the IFAD VDM-SL Toolbox. Master’s thesis, Technical University Graz, Austria (March 1997)

    Google Scholar 

  16. Giesl, J.: Termination of nested and mutually recursive algorithms. Journal of Automated Reasoning 19, 10–29 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  17. Slind, K.: Another look at nested recursion. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 498–518. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  18. Dennis, L.A., Collins, G., Norrish, M., Boulton, R., Slind, K., Robinson, G., Gordon, M., Melham, T.: The PROSPER Toolkit. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  19. Agerholm, S., Sunesen, K.: Formalizing a Subset of VDM-SL in HOL. Technical report, IFAD (April 1999)

    Google Scholar 

  20. Agerholm, S., Sunesen, K.: Reasoning about VDM-SL Proof Obligations in HOL. Technical report, IFAD (1999)

    Google Scholar 

  21. Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS System Guide - Version 2.4 (2001)

    Google Scholar 

  22. Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language Reference - Version 2.4 (2001)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Aarhus School of Engineering, Aarhus University, Denmark

    Augusto Ribeiro & Peter Gorm Larsen

Authors
  1. Augusto Ribeiro
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Peter Gorm Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing, Computer Science Dept, National University of Singapore, 13 Computing Drive, 117417, Singapore, Singapore

    Jin Song Dong

  2. Software Engineering Institute, East China Normal University, 3663 Zhongshan Road (North), 200062, Shanghai, China

    Huibiao Zhu

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ribeiro, A., Larsen, P.G. (2010). Proof Obligation Generation and Discharging for Recursive Definitions in VDM. In: Dong, J.S., Zhu, H. (eds) Formal Methods and Software Engineering. ICFEM 2010. Lecture Notes in Computer Science, vol 6447. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16901-4_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-16901-4_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-16900-7

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation