Representing, Verifying and Applying Software Development Steps using the PVS System

In this paper generic software development steps of different complexity are represented and verified using the (higher-order, strongly typed) specification and verification system PVS. The transformations considered in this paper include large powerful steps encoding general algorithmic paradigms as well as smaller transformations for the operationalization of a descriptive specification. The application of these transformation patterns is exemplified by means of simple examples. Furthermore, we show how to guide proofs of correctness assertions about development steps. Finally, this work serves as a case-study and test for the usefulness of the PVS system.

Available as Postscript (128 KB) or compressed Postscript (48 KB)

@InProceedings{Dold95,

  author = "Axel Dold",

  title = "Representing, Verifying and Applying Software Development Steps 
              using the PVS System",

  volume = "936",

  series = "Lecture Notes in Computer Science",

  pages = "431--435",

  booktitle = "Proceedings of the Fourth International Conference on 
                Algebraic Methodology and Software Technology, AMAST'95, Montreal",

  year = "1995",

  publisher = "Springer-Verlag",

  editor = "V.S. Alagar and Maurice Nivat"
}