期刊文献+

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

Program Developing System with Theorem Prover Embedded in
在线阅读 下载PDF
导出
摘要 提出了一个基于重写技术的程序开发系统,它提供了扩展的函数式语言和代数规约语言相结合的混合语言,该语言中引入了优化规则和测试等式说明机制.优化规则用于优化代码和满足某些特殊需求.运用测试等式说明机制可使程序员在程序中给出一些用于测试的等式,对程序进行测试,这些测试是在被开发系统形成前进行的.对优化规则和测试等式的证明,是由系统中的证明子系统(定理证明器)完成的.定理证明器的引入,提高了所开发系统的正确性,并且有利于缩短系统的开发周期. 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.
出处 《上海交通大学学报》 EI CAS CSCD 北大核心 1998年第10期42-45,共4页 Journal of Shanghai Jiaotong University
基金 国家九五科技攻关基金
关键词 函数式语言 软件工程 程序开发系统 定理证明器 functional language algebraic specification rewriting system theorem proving test
  • 相关文献

参考文献4

  • 1邵志清,博士学位论文,1998年
  • 2孙永强,ACM SIGPLAN Not,1997年,32卷,2期,27页
  • 3陆朝俊,博士学位论文,1994年
  • 4邵志清,J Comput Sci Technol

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部