两次数据精化的形式化软件开发方法 (2006年)

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