Software Development in PVS Using Generic Development Steps

  • Axel Dold
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1766)


This paper is concerned with a mechanized formal treatment of the transformational software development process in a unified framework. We utilize the PVS system to formally represent, verify and correctly apply generic software development steps and development methods from different existing transformational approaches. We illustrate our approach by representing the well-known divide-and-conquer paradigm, two optimization steps, and by formally deriving a mergesort program.


formal verification mechanized theorem proving generic development steps transformational software development 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Klaus Achatz and Helmuth Partsch. From descriptive specifications to operational ones: A powerful transformation rule, its applications and variants. Technical Report 96-13, Universität Ulm, December 1996.Google Scholar
  2. 2.
    Richard S. Bird. The promotion and accumulation strategies in transformational programming. ACM—Transactions on Programming Languages and Systems, 6(4):487–504, 1984.MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Axel Dold. Representing, Verifying and Applying Software Development Steps using the PVS System. In V.S. Alagar and Maurice Nivat, editors, Proceedings of the Fourth International Conference on Algebraic Methodology and Software Technology, AMAST’95, Montreal, volume 936 of Lecture Notes in Computer Science, pages 431–445. Springer-Verlag, 1995.CrossRefGoogle Scholar
  4. 4.
    Berthold Hoffmann and Bernd Krieg-Brückner (Eds.). Program Development by Specification and Transformation—The PROSPECTRA Methodology, Language Family, and System, volume 680 of Lecture Notes in Computer Science. Springer-Verlag, 1993.zbMATHGoogle Scholar
  5. 5.
    G. Huet and B. Lang. Proving and applying program transformations expressed with second-order-patterns. Acta Informatica, 11:31–55, 1978.MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Kolyang, B. Wolff, and T. Santen. Correct and User-Friendly Implementations of Transformation Systems. In J. Woodcock M.-C. Gaudel, editor, FME’96: Industrial Benefit and Advances in Formal Methods, volume 1051 of Lecture Notes in Computer Science, pages 629–648, 1996.CrossRefGoogle Scholar
  7. 7.
    C. Kreitz. Metasynthesis—deriving programs that develop programs. Technical Report AIDA-93-03, Fachgebiet Intellektik, Technische Hochschule Darmstadt, 1993.Google Scholar
  8. 8.
    S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, February 1995.CrossRefGoogle Scholar
  9. 9.
    S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748–752, Saratoga NY, 1992. Springer-Verlag.Google Scholar
  10. 10.
    Helmuth A. Partsch. Specification and Transformation of Programs—A Formal Approach to Software Development. Texts and Monographs in Computer Science. Springer-Verlag, 1990.Google Scholar
  11. 11.
    H. Rueß. Formal meta-programming in the calculus of constructions. PhD thesis, Universität Ulm, Fakultät für Informatik, 1995.Google Scholar
  12. 12.
    N. Shankar. Steps towards mechanizing program transformations using PVS. Science of Computer Programming, 26(1–3):33–57, 1996.CrossRefGoogle Scholar
  13. 13.
    Douglas R. Smith. Applications of a strategy for designing divide-and-conquer algorithms. Science of Computer Programming, 8(3):213–229, 1987.CrossRefzbMATHGoogle Scholar
  14. 14.
    Douglas R. Smith. KIDS—a semi-automatic program development system. IEEE—Transactions on Software Engineering, Special Issue on Formal Methods in Software Engineering, 16(9):1024–1043, September 1990.Google Scholar
  15. 15.
    Douglas R. Smith and Michael R. Lowry. Algorithm theories and design tactics. Science of Computer Programming, 14(2–3):305–321, 1990.MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Mitchell Wand. Continuation-based program transformation strategies. Journal of the ACM, 27(1):164–180, January 1980.MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Axel Dold
    • 1
  1. 1.Fakultät für InformatikUniversität UlmUlmGermany

Personalised recommendations