Program Development and Verification Based on Rewriting Techniques
Sun Yong · 2000
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.