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 illustrated 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

• amast95.ps