變換模型

為了確認形式化規格説明與軟件需求的一致性，往往以形式化規格説明為基礎開發一個軟件模型。用户可以從人機界面、系統主要功能、性能等幾個方面對原型進行評審。必要時，可以對軟件需求、形式化規格説明和原型進行修改，直至原型被確認時為止。這時軟件開發人員就可以對形式化的規格説明進行一系列的程序變換，直至生成計算機系統可以接受的目標代碼。

程序變換是軟件開發的另一種方法，其基本思想是把程序設計的過程分為生成階段和改進階段。首先通過對問題的分析制定形式規範，並生成一個程序，通常是一種函數型的“遞歸方程”；然後通過一系列保持正確性的源程序到源程序的變換，把函數型風格轉換成過程型風格，並進行數據結構和算法的求精，最終得到一個有效的面向過程的程序。這種變換過程是一種嚴格的形式推導過程，所以只需對變換前的程序規範加以驗證，變換後的程序的正確性將由變換法則的正確性來保證。

變換模型的優點是解決了diam結構經多次修改而變壞的問題，減少了許多中間步驟（如設計、編碼、測試等）。但是，變換模型仍有較大侷限性，以形式化開發方法為基礎的變換模型需要嚴格的數學理論和一整套開發環境的支持，形化開發方法在理論、實踐和人員培訓方面離工程應用尚有一段距離。