The program development preocess of stepwise specification, transformation and verification consists of two transitions. One is from the informal requirement to the formal specificaiton, the other is from the formal specification to the algorithmic implementation. The key point in the development process is how to make design decisions. In order to maintain and adapt software and to verify, not only should the specification and the implementation be recorded, but also the design decisions made during the development.We give two examples to demonstrate this methodo;ogy and how the design decisions take role in it.An environment which includes several subsystems called SPEC,PROT,VERI,and OOMM is implemented to support the above process.