| 摘要: |
| 完整地介绍了一个基于重写技术的程序开发和验证系统,重点展示验证子系统的理论、方法 和技术.验证子系统使得系统能自动证明程序和规范中的优化规则及测试等式,从而进一步保 证程序开发过程的正确性.验证子系统所采用的主要技术是以成批证明方法和证据测试集为 特色的重写归纳方法. |
| 关键词: 函数程序设计语言,代数规范,项重写系统,定理 证明,无归纳的归纳法. |
| DOI： |
| 分类号: |
| 基金项目:本文研究得到国家“九五”重点科技攻关项目基金(No.96-729-01-06)资助. |
|
| Program Development and Verification Based on Rewriting Techniques |
|
SUN Yong-qiang,LU Chao-jun,SHAO Zhi-qing
|
| 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. |
| Key words: Functional programming language, algebraic specification, term rewriting system, theorem proving, inductionless induction. |
