Software Development in PVS Using Generic Development Steps
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.
Keywordsformal verification mechanized theorem proving generic development steps transformational software development
Unable to display preview. Download preview PDF.
- 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
- 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
- 7.C. Kreitz. Metasynthesis—deriving programs that develop programs. Technical Report AIDA-93-03, Fachgebiet Intellektik, Technische Hochschule Darmstadt, 1993.Google Scholar
- 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.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.H. Rueß. Formal meta-programming in the calculus of constructions. PhD thesis, Universität Ulm, Fakultät für Informatik, 1995.Google Scholar
- 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