使用显式策略进行程序构造

摘要

本文提出一种交互式的程序(半)自动综合方法:使用显式策略引导系统进行程序构造。这些策略包括程序员提供的问题求解策略和系统内部的标准策略,如数学归纳法、归结方法和程序变换规则/策略。策略都用高阶函数式元语言TSL/ML统一地描述,它们的施用则通过高阶一致化完成。因此,我们的程序综合方法可以在统一的框架下使用多种软件自动构造技术,且易于自动实现。