| 基于Tableau方法的程序综合系统——DTPS |
| |
| 引用本文： | 赵莹 全炳哲. 基于Tableau方法的程序综合系统——DTPS[J]. 计算机研究与发展, 1997, 34(8): 577-581 |
| |
| 作者姓名： | 赵莹 全炳哲 |
| |
| 作者单位： | 吉林大学计算机科学系 |
| |
| 基金项目： | “863”计划和国家自然科学基金 |
| |
| 摘 要： | 本文简单介绍了基于Ｔａｂｌｅａｕ方法的程序综合系统－ＤＴＰＳ．ＤＴＰＳ系统以定理证明为基础，为构造一个满足程序规约的程序，只需证明的确存在一个满足条件的对象。如果这个证明存在，那么从证明中可抽取出一个满足该程序规约的程序。
|
| 关 键 词： | Tableau方法 程序综合系统 DTPS 软件自动化 |
DTPS: A PROGRAM SYNTHESIS SYSTEM BASED ON TABLEAU METHOD |
| |
| ZHAO Ying QUAN Bing Zhe JIN Chun Zhao. DTPS: A PROGRAM SYNTHESIS SYSTEM BASED ON TABLEAU METHOD[J]. Journal of Computer Research and Development, 1997, 34(8): 577-581 |
| |
| Authors: | ZHAO Ying QUAN Bing Zhe JIN Chun Zhao |
| |
| Abstract: | 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. |
| |
| Keywords: | program synthesis theorem proving Tableau method |
| 本文献已被 CNKI 维普 等数据库收录！ |
