两次数据精化的形式化软件开发方法  

A Formal Software Development Method of Using Data Refinement With Two Times

作　　者：邢小英[1] 王维维[1] 

机构地区：[1]浙江大学计算机系

出　　处：《计算机工程》2006年第1期102-104,共3页Computer Engineering

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

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]