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

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

Program Development and Verification Based on Rewriting Techniques

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.