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

Program Development and Verification Based on Rewriting Techniques

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

In this paper, the authors present a complete introduction of a program development and verification system based on rewriting techniques, focusing on the theory, methods and techniques of the verification subsystem. The verification subsystem enables the system to prove the correctness of the optimization rules and test equations in programs and specifications, hence the soundness of the program development process is further guaranteed. The main technique employed in the verification subsystem is rewriting induction featuring batch proof method and witnessed test sets.