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

• 作者: 孙永强 邵志清 陆朝俊
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 函数程序设计语言 代数规范 项重写系统 定理 证明 无归纳的归纳法
• 年，卷（期）: 2000,（8）
• 页码范围: 1066-1070
• 页数: 5页
• 分类号: TP311
• 字数: 4773字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陆朝俊	上海交通大学计算机科学与工程系	7	33	4.0	5.0
2	孙永强	上海交通大学计算机科学与工程系	72	373	10.0	15.0
3	邵志清	华东理工大学计算机系	90	761	14.0	24.0