摘要： 提出了一种从数据精化、过程精化、再数据精化的两次数据精化的形式化软件开发方法。传统Z 规约数据精化很复杂。该文先采用过程写出初始规范，对模式进行第一次数据精化，然后把它转换为Z 模式，再进行过程精化。最后再数据精化到目标代码。以常见动态Web 网页脚本语言PHP 为例，阐述了该方法。并为此写了一套从过程到Z 模式的转化规则，以及精化到PHP 的精化规则。

关键词: 过程；Z 语言；规范；精化演算；PHP

Abstract: A formal software development method of using data refinement with two times is introduced, which from data refinement to process refinement then to data refinement.The tradition data refinement in Z is very complexity.So this article writes initial specification in procedure and implementes the first data refinement, then translates it into Z frame and implementes process refinement.Finally it developes abstract programs into executable code.Web language of PHP is an example.Translation rules from process to Z frame and from abstract programs to PHP are written.

Key words: Procedure; Z language; Specification; Refinement calculus; PHP