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

Program Developing System with Theorem Prover Embedded in

作　　者：孙永强[1] 杨继锋[1] 陆朝俊[1] 邵志清[2] 

机构地区：[1]上海交通大学计算机科学与工程系 [2]华东理工大学计算机科学系

出　　处：《上海交通大学学报》1998年第10期42-45,共4页Journal of Shanghai Jiaotong University

基　　金：国家九五科技攻关基金

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

关 键 词：函数式语言 软件工程 程序开发系统 定理证明器 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]