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.

Online Copy

Postscript (169 KB).

BibTeX Entry

@InProceedings{Dold98, author = "Axel Dold" title = "Software Development in PVS using Generic Development Steps", series = "Lecture Notes in Computer Science", number = "1766", pages = "146--161", booktitle = "Generic Programming - International Seminar on Generic Programming" publisher = "Springer-Verlag", }