是否存在有益的错误？CEGIS 的理论分析

反例引导归纳综合（CEGIS）用于从候选程序空间中综合程序。如果候选程序空间是有限的，该技术保证终止并综合出正确的程序；但如果候选程序空间是无限的，该技术可能终止也可能不终止，且不一定能综合出正确的程序。在本文中，我们对反例引导归纳综合技术进行了理论分析。我们研究了使用 CEGIS 能够综合出正确程序的候选空间集合是否依赖于归纳综合中使用的反例，即是否存在能够增强综合能力的“有益错误”。我们研究了使用最小反例而非任意反例是否会扩大归纳综合能够成功综合出正确程序的候选程序空间集合。我们考虑两种反例：最小反例和历史有界反例。CEGIS 任何迭代中使用的历史有界反例受归纳综合先前迭代中使用的示例所限制。我们考察了这两种情况下归纳综合能力的相对变化。我们表明，使用最小反例的综合技术 MinCEGIS 具有与 CEGIS 相同的综合能力，而使用历史有界反例的综合技术 HCEGIS 具有不同于 CEGIS 的综合能力，但两者互不占优。