| 摘要: |
| 本文提出一种交互式的程序(半)自动综合方法:使用显式策略引导系统进行程序构造。这些策略包括程序员提供的问题求解策略和系统内部的标准策略,如数学归纳法、归结方法和程序变换规则/策略。策略都用高阶函数式元语言TSL/ML统一地描述,它们的施用则通过高阶一致化完成。因此,我们的程序综合方法可以在统一的框架下使用多种软件自动构造技术,且易于自动实现。 |
| 关键词: |
| DOI： |
| 分类号: |
| 基金项目:本项研究得到“八六三”计划“软件生成自动化”项目和国家自然科学基金的部分资助 |
|
| USING EXPLICIT STRATEGIES TO GUIDE PROGRAM CONSTRUCTION |
|
Tan Qingping,Chen Huowang
|
| Abstract: |
| In this paper we propose an interactive approach to program synthesis: Explicit strategies are used to guide program construction. Our approach regards program synthesis as a constructive theorem proving task. By specifying proof strategies in a higher order functional meta-language, we are able to represent the programmer s advice, mathematical inductions, program transformation rules/strategies and resolution methods in a uniform manner. The implementation of strategies depends on higher order unification.Our approach can be automatized easily. |
| Key words: |
