JOOADL方法中循环程序的构造

循环结构的生成是基于程序规范的构造方法的核心问题之一。ＪＯＯＡＤＬ方法在规范说明中用一种类一阶谓词逻辑公式描述参数所满足的条件和目标，并提供一种将目标对应到程序的方法。其中将含量词的子公式对应到循环结构，循环索引变元遍历有界约束变元的取值域。本文试探讨循环结构生成方法的一个改进途径：利用关于量词所在类上的断言集，通过由目标制导的演绎，得到启发式，以指导生成更有效的循环程序。

SYNTHESIZING LOOP STRUCTURES IN JOOADL

The construction of loop structures is one of the key issues in program synthesis based on specifications. JOOADL applies first - order- logic - like formulas to program specifications for describing conditions and target, and offers a formalism mapping the target (and subtargets) to programs. In this method,the quantified subtargets are mapped to loop structures, in which each index variable tries to go through the variation domain of the corresponding quantified variable. This paper discusses an improved approach for constructing loop structures in JOOADL framework. It uses assertions on the sorts of the variables to obtain some heuristics by target - guided deductions. These heuristics will in turn guide the constructions of more efficient loop structures.