基于Tableau方法的程序综合系统──DTPS  

DTPS: A PROGRAM SYNTHESIS SYSTEM BASED ON TABLEAU METHOD

作　　者：赵莹[1] 全炳哲[1] 金淳兆[1] 

机构地区：[1]吉林大学计算机科学系

出　　处：《计算机研究与发展》1997年第8期577-581,共5页Journal of Computer Research and Development

基　　金："863"计划和国家自然科学基金

摘　　要：本文简单介绍了基于Ｔａｂｌｅａｕ方法的程序综合系统——ＤＴＰＳ．ＤＴＰＳ系统以定理证明为基础，为构造一个满足程序规约的程序，只需证明的确存在一个满足条件的对象．如果这个证明存在，那么从证明中可抽取出一个满足该程序规约的程序．This paper introduces a tableau method based program system,called DTPS.Based on mechanical theorem proving techniques, DTPS proves the existence of an object meeting the specified conditions in order to construct a program meeting a specification.If the proof exists, the program derived from the proof not only meets the specification, but also is free from logical error.

关 键 词：TABLEAU方法 程序综合系统 DTPS 软件自动化 

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