形式规范语言数据求精过程的代数验证方法

软件求精技术是实现从形式规范语言到可执行代码转换的一种重要技术。规范语言的求精过程可分为数据求精和过程求精。从面向模型的规范语言 (如VDM ,Z)出发 ,提出一种严格定义的类型代数理论和一组基于抽象代数的规则来验证数据求精过程 ,解决了形式规范语言在数据转换过程中的语言一致性问题。