基于重写技术的程序开发与验证

摘要：

完整地介绍了一个基于重写技术的程序开发和验证系统,重点展示验证子系统的理论、方法和技术.验证子系统使得系统能自动证明程序和规范中的优化规则及测试等式,从而进一步保证程序开发过程的正确性.验证子系统所采用的主要技术是以成批证明方法和证据测试集为特色的重写归纳方法.

关键词：函数程序设计语言、代数规范、项重写系统、定理 证明、无归纳的归纳法

所属期刊栏目：11

分类号：TP311(计算技术、计算机技术)

资助基金：国家科技攻关项目96-729-01-06

在线出版日期：2004-01-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：1066-1070