图示
　　


　　　　　　　　　　　　　　　　　图1.10 变换模型

　　软件需求确定以后，可用某种形式化的需求规格说明语言（如VDM的META-Ⅳ，CSP和Z）描述软件需求规格说明，生成形式化的设计说明。为了确认形式化规格说明与软件需求的一致性，往往以形式化设计说明为基础开发一个软件原型。用户可以从人机界面、系统主要功能、性能等几个方面对原型进行评审，必要时，可以对软件需求、形式化设计说明和原型进行修改，直到原型被确认为止。这时软件开发人员就可以对形式化的规格说明进行一系列的程序变换，直到生成计算机可以接受的目标代码。

　　多步程序变换过程的一个重要性质是每一步变换对相关的模型描述是"封闭的"。即每一步程序变换的正确性仅与该步变换所依据的规范Mi以及对变换后的假设Mi+1有关，在此意义上，变换步骤独立于其他变换步骤。这称为变换的独立性。若没有这种独立性，就不能控制错误的蔓延。