Skip to main content
SpringerLink
Log in

Sound and Complete Verification Condition Generator for Functional Recursive Programs

  • Chapter
  • First Online:
Numerical and Symbolic Scientific Computing

Part of the book series: Texts & Monographs in Symbolic Computation ((TEXTSMONOGR))

  • 1489 Accesses

Abstract

We present a method for verifying recursive functional programs by defining a verification condition generator (VCG) which covers the most frequent type of recursive programs. These programs may operate on arbitrary domains. We prove soundness and completeness of the VCG and this provides a warranty that any system based on our results will be sound. We introduce here the notion of completeness of a VCG as a duality of soundness. Completeness is important for the following two reasons: theoretically, it is the dual of soundness and practically, it helps debugging. Any counterexample for the failing verification condition will carry over to a counterexample for the given program and specification. Moreover, the failing proof gives information about the place of the bug. Furthermore, we introduce a specialized strategy for termination. The termination problem is reduced to the termination of a simplified version of the program. The conditions for the simplified versions are identical for special classes of functional programs, thus they are highly reusable.

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 EPUB and 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

Notes

  1. 1.

    This approach is in fact borrowed from the Theorema system.

References

  1. ACL2. http://www.cs.utexas.edu/users/moore/acl2/

  2. de Bakker, J.W., Scott, D.: A Theory of Programs. In IBM Seminar, Vienna, Austria (1969)

    Google Scholar 

  3. Bernhard, B., Reiner, H., Peter, H.S. (ed.): Verification of Object-Oriented Software: The KeY Approach. vol. 4334, LNCS, Springer (2007)

    Google Scholar 

  4. Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Springer, Berlin (2004)

    Google Scholar 

  5. Blanqui, F., Hinderer, S., Coupet-Grimal, S., Delobel, W., Kroprowski, A.: CoLoR, a Coq Library on Rewriting and Termination. In: Geser, A., Søndergaard, H. (eds.) Proceedings of 8th International Workshop on Termination, Seattle, WA, USA (2006)

    Google Scholar 

  6. Boyer, R.S., Moore, J.S.: A Computational Logic Handbook. Academic Press Professional, Incorporation, San Diego, CA, USA (1988)

    MATH  Google Scholar 

  7. Buchberger, B.: Algorithm Supported Mathematical Theory Exploration: A Personal View and Stragegy. In: Buchberger, B. John Campbell, (eds.) Proceedings of AISC 2004 (7th International Conference on Artificial Intelligence and Symbolic Computation), Springer Lecture Notes in Artificial Intelligence, vol. 3249, pp. 236–250. Springer, Berlin 22–24 (2004)

    Google Scholar 

  8. Buchberger, B.: Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal (An Algorithm for Finding the Basis Elements in the Residue Class Ring Modulo a Zero Dimensional Polynomial Ideal). PhD thesis, Mathematical Institute, University of Innsbruck, Austria (1965). (English translation Journal of Symbolic Computation 41 (2006) 475–511).

    Google Scholar 

  9. Buchberger, B.: Gröbner-Bases: An Algorithmic Method in Polynomial Ideal Theory. In: Bose, N.K. (eds.) Multidimensional Systems Theory – Progress, Directions and Open Problems in Multidimensional Systems, pp. 184–232. Reidel Publishing Company, Dodrecht, Boston, Lancaster (1985)

    Google Scholar 

  10. Buchberger, B.: Towards the Automated Synthesis of a Groebner Bases Algorithm. RACSAM – Revista de la Real Academia de Ciencias (Review of the Spanish Royal Academy of Science), Serie A: Mathematicas, 98(1), 65–75 (2004)

    Google Scholar 

  11. Buchberger, B., Affenzeller, M., Ferscha, A., Haller, M., Jebelean, T., Klement, E.P., Paule, P., Pomberger, G., Schreiner, W., Stubenrauch, R., Wagner, R., Weiß, G., Windsteiger, W.: Hagenberg Research. Springer, 1st edition (2009)

    Google Scholar 

  12. Buchberger, B., Craciun, A., Jebelean, T., Kovacs, L., Kutsia, T., Nakagawa, K., Piroi, F., Popov, N., Robu, J., Rosenkranz, M., Windsteiger, W.: Theorema: Towards Computer-Aided Mathematical Theory Exploration. J. Appl. Logic pp. 470–504 (2006)

    Google Scholar 

  13. Buchberger, B., Dupre, C., Jebelean, T., Kriftner, F., Nakagawa, K., Vasaru, D., Windsteiger, W.: The Theorema Project: A Progress Report. In Calculemus 2000: Integration of Symbolic Computation and Mechanized Reasoning, Calculemus (2000)

    Google Scholar 

  14. Buchberger, B., Lichtenberger, F.: Mathematics for Computer Science I – The Method of Mathematics (in German). Springer, 2nd edition (1981)

    Google Scholar 

  15. Chlipala, A.: A Verified Compiler for an Impure Functional Language. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’10), pp. 237–248. New York, NY, USA (2010)

    Google Scholar 

  16. Floyd, R.W.: Assigning Meanings to Programs. In Proceedings of Symphosia in Applied Mathematics 19, pp. 19–37 (1967)

    Article  MathSciNet  Google Scholar 

  17. Gordon, M.: From LCF to HOL: A Short History. pp. 169–185. MIT Press, MA, USA (2000)

    Google Scholar 

  18. Greibach, S.A.: Theory of Program Structures: Schemes, Semantics, Verification. Springer, New York, Secaucus, NJ, USA (1985)

    MATH  Google Scholar 

  19. Hildebrand, B.F.: Introduction to Numerical Analysis: 2nd Edition. Dover Publications, New York, NY, USA (1987)

    MATH  Google Scholar 

  20. Hoare, C.A.R.: An axiomatic basis for computer programming. Comm. ACM 12(10), 576–580 (1969)

    Article  MATH  Google Scholar 

  21. HOL. http://hol.sourceforge.net/

  22. Homeier, P.V., Martin, D.F.: Secure Mechanical Verification of Mutually Recursive Procedures. Inf. Comput. 187(1), 1–19 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  23. Neil, I.: Computability and Complexity. In: Edward, N. Zalta, (eds) The Stanford Encyclopedia of Philosophy (Fall 2008 Edition). http://plato.stanford.edu/archives/fall2008/entries/computability

  24. Kaufmann, M., Moore, J.S.: An Industrial Strength Theorem Prover for a Logic Based on Common Lisp. Software Eng. 23(4), 203–213 (1997)

    Article  Google Scholar 

  25. Langford, W.J., Broadbent, T.A.A., Goodstein, R.L.: Obituary: Professor Eric Harold Neville. Math. Gaz. 48(364), 131–145 (1964)

    Google Scholar 

  26. Rustan, K., Leino, M., Peter, M., Jan, S.: Verification of Concurrent Programs with Chalice. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) Foundations of Security Analysis and Design V, pp. 195–222. Springer, New York (2009)

    Google Scholar 

  27. Loeckx, J., Sieber, K.: The Foundations of Program Verification. Teubner, 2nd edition (1987)

    Google Scholar 

  28. Luckham, D.C., Park, D.M.R., Paterson, M.: On Formalised Computer Programs. J. Comput. Syst. Sci. 4(3), 220–249 (1970)

    Article  MathSciNet  MATH  Google Scholar 

  29. Manna, Z.: Mathematical Theory of Computation. McGraw-Hill, New York (1974)

    MATH  Google Scholar 

  30. Matthews, J., Moore, J.S., Ray, S., Vroon, D.: Verification Condition Generation Via Theorem Proving. In: Hermann, M., Voronkov, A. (eds.) In Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2006), LNCS, vol. 4246, pp. 362–376. Phnom Penh, Cambodia (2006)

    Chapter  Google Scholar 

  31. Meyer, B.: Applying design by contract. Computer 25(10), 40–51 (1992)

    Article  Google Scholar 

  32. Neville, E.H.: Iterative Interpolation. J. Indian Math. Soc. 20, 87–120 (1934)

    Google Scholar 

  33. Peter, R.: Rekursive Funktionen in der Komputer-Theorie. Verlag d. ungarisch. Akademie d. Wiss., Budapest (1976)

    Google Scholar 

  34. Press, W.H., Teukolsky, S.A., Vetterling, W.T., Flannery, B.P.: Numerical Recipes in C: The Art of Scientific Computing. Cambridge University Press, 2 edition (1992)

    Google Scholar 

  35. PVS group: PVS Specification and Verification System. http://pvs.csl.sri.com (2004)

  36. Smith, D.R.: Top-Down Synthesis of Divide-and-Conquer algorithms. Artif. Intell. 27(1), 43–96 (1985)

    Article  MATH  Google Scholar 

  37. Sunrise: http://www.cis.upenn.edu/\~hol/sunrise/

  38. van der Voort, M.: Introducing Well-founded Function Definitions in HOL. In Higher Order Logic Theorem Proving and its Applications: Proceedings of the IFIP TC10/WG10.2 Workshop, pp. 117–132 (1992)

    Google Scholar 

  39. Walter, S.B., Lawrence, H.L.: Theory of Computation. Wiley, New York, NY, USA (1974)

    Google Scholar 

  40. Wiedijk, F. (ed.): The Seventeen Provers of the World, Foreword by Dana, S. Scott, Lecture Notes in Computer Science. vol. 3600, Springer (2006)

    Google Scholar 

  41. Zee, K., Kuncak, V., Rinard, M.C.: Full Functional Verification of Linked Data Structures. In Proceedings of the 30th ACM Conference on Programming Language Design and Implementation, pp. 349–361 (2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria

    Nikolaj Popov & Tudor Jebelean

Authors
  1. Nikolaj Popov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tudor Jebelean
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nikolaj Popov .

Editor information

Editors and Affiliations

  1. Inst. Numerische Mathematik, Universität Linz, Altenbergerstr. 69, Linz, 4040, Austria

    Ulrich Langer

  2. , Research Institute for Symbolic Computat, Johannes Kepler University, Altenbergerstr. 69, Linz, 4040, Austria

    Peter Paule

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag/Wien

About this chapter

Cite this chapter

Popov, N., Jebelean, T. (2012). Sound and Complete Verification Condition Generator for Functional Recursive Programs. In: Langer, U., Paule, P. (eds) Numerical and Symbolic Scientific Computing. Texts & Monographs in Symbolic Computation. Springer, Vienna. https://doi.org/10.1007/978-3-7091-0794-2_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-7091-0794-2_11

  • Published:

  • Publisher Name: Springer, Vienna

  • Print ISBN: 978-3-7091-0793-5

  • Online ISBN: 978-3-7091-0794-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation