首页 | 本学科首页   官方微博 | 高级检索  
     

基于重写技术的程序开发与验证
引用本文:孙永强,陆朝俊,邵志清. 基于重写技术的程序开发与验证[J]. 软件学报, 2000, 11(8): 1066-1070
作者姓名:孙永强  陆朝俊  邵志清
作者单位:1. 上海交通大学计算机科学与工程系,上海,200030
2. 华东理工大学计算机系,上海,200237
基金项目:本文研究得到国家“九五”重点科技攻关项目基金(No.96-729-01-06)资助.
摘    要:完整地介绍了一个基于重写技术的程序开发和验证系统,重点展示验证子系统的理论、方法 和技术.验证子系统使得系统能自动证明程序和规范中的优化规则及测试等式,从而进一步保 证程序开发过程的正确性.验证子系统所采用的主要技术是以成批证明方法和证据测试集为 特色的重写归纳方法.

关 键 词:函数程序设计语言  代数规范  项重写系统  定理 证明  无归纳的归纳法.
收稿时间:2000-01-17
修稿时间:2000-05-12

Program Development and Verification Based on Rewriting Techniques
SUN Yong-qiang,LU Chao-jun and SHAO Zhi-qing. Program Development and Verification Based on Rewriting Techniques[J]. Journal of Software, 2000, 11(8): 1066-1070
Authors:SUN Yong-qiang  LU Chao-jun  SHAO Zhi-qing
Affiliation:SUN Yong|qiang LU Chao jun 1 SHAO Zhi qing 2 1 (Department of Computer Science and Engineering Shanghai Jiaotong University Shanghai 200030
Abstract:In this paper, the authors present a complete introduction of a program developm ent and verification system based on rewriting techniques, focusing on the theor y, methods and techniques of the verification subsystem. The verification subsys tem enables the system to prove the correctness of the optimization rules and te st equations in programs and specifications, hence the soundness of the program development process is further guaranteed. The main technique employed in the ve rification subsystem is rewriting induction featuring batch proof method and wit nessed test sets.
Keywords:Functional programming language   algebraic specification   term rewriting system   theorem proving   inductionless induction.
本文献已被 CNKI 维普 万方数据 等数据库收录!
点击此处可从《软件学报》浏览原始摘要信息
点击此处可从《软件学报》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号