内含定理证明器的程序开发系统

提出了一个基于重写技术的程序开发系统，它提供了扩展的函数式语言和代数规约语言相结合的混合语言，该语言中引入了优化规则和测试等式说明机制．优化规则用于优化代码和满足某些特殊需求．运用测试等式说明机制可使程序员在程序中给出一些用于测试的等式，对程序进行测试，这些测试是在被开发系统形成前进行的．对优化规则和测试等式的证明，是由系统中的证明子系统（定理证明器）完成的．定理证明器的引入，提高了所开发系统的正确性，并且有利于缩短系统的开发周期．

Program Developing System with Theorem Prover Embedded in

As a rewriting techniques based program development system, it provides an enhanced functional language and algebraic specification language mixed language. The language has optimal rule and test equation declaration mechanisms. The optimal rule can optimize code and satisfy special requirements. By the test equation declaration mechanism, programmer can test the program by giving some test equations in the program. The testing is performed before the generation of the executable code. The proving of optimal rule and test equation is performed by a theorem prover which can help to improve the correctness of program and to shorten the program development cycle time.