University of Ulm, Faculty of Computer Science, Dept. of Artificial Intelligence up: Dept. of AI

Software Development in PVS using Generic Development Steps

Axel Dold

In Generic Programming - International Seminar on Generic Programming
Schloss Dagstuhl, April 27 - May 1, 1998.
Springer LNCS 1766.
© Springer-Verlag


 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.

 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",
}


Dept. of AI Homepage Research Help Mail to Webmaster A. Dold - Oct 5, 2000.