Abstract
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.
This work has been partially supported by the Deutsche Forschungsgemeinschaft (DFG) project Verifix.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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.
Richard S. Bird. The promotion and accumulation strategies in transformational programming. ACM—Transactions on Programming Languages and Systems, 6(4):487–504, 1984.
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.
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.
G. Huet and B. Lang. Proving and applying program transformations expressed with second-order-patterns. Acta Informatica, 11:31–55, 1978.
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.
C. Kreitz. Metasynthesis—deriving programs that develop programs. Technical Report AIDA-93-03, Fachgebiet Intellektik, Technische Hochschule Darmstadt, 1993.
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.
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.
Helmuth A. Partsch. Specification and Transformation of Programs—A Formal Approach to Software Development. Texts and Monographs in Computer Science. Springer-Verlag, 1990.
H. Rueß. Formal meta-programming in the calculus of constructions. PhD thesis, Universität Ulm, Fakultät für Informatik, 1995.
N. Shankar. Steps towards mechanizing program transformations using PVS. Science of Computer Programming, 26(1–3):33–57, 1996.
Douglas R. Smith. Applications of a strategy for designing divide-and-conquer algorithms. Science of Computer Programming, 8(3):213–229, 1987.
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.
Douglas R. Smith and Michael R. Lowry. Algorithm theories and design tactics. Science of Computer Programming, 14(2–3):305–321, 1990.
Mitchell Wand. Continuation-based program transformation strategies. Journal of the ACM, 27(1):164–180, January 1980.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dold, A. (2000). Software Development in PVS Using Generic Development Steps. In: Jazayeri, M., Loos, R.G.K., Musser, D.R. (eds) Generic Programming. Lecture Notes in Computer Science, vol 1766. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-39953-4_12
Download citation
DOI: https://doi.org/10.1007/3-540-39953-4_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41090-4
Online ISBN: 978-3-540-39953-7
eBook Packages: Springer Book Archive