一句话：提出导航式编程合成问题，保证规约细化中所有且仅有有效下一步，并高效求解。
当程序合成任务从歧义的规约出发时，合成过程通常需要迭代细化规约以找到特定目标解。本文提出“导航式编程合成问题”（Programming by Navigation Synthesis Problem），专门支持这种迭代规约细化。与已有工作不同，作者证明满足该问题的合成器在每一步都展示所有有效下一步（强完备性）且仅展示有效下一步（强可靠）。为求解该问题，本文将经典逻辑风格的类型居留（type inhabitation）oracle 转化为完全构造性的程序合成器，并通过可靠编译到 Datalog 来定义该 oracle。实证评估表明，该技术实现了一个高效的导航式编程合成器，能求解基线方法无法完成或规模过大的任务，并且是首个保证规约细化过程同时满足强完备性与强可靠性的合成器。
When a program synthesis task starts from an ambiguous specification, the synthesis process often involves an iterative specification refinement process. We introduce the Programming by Navigation Synthesis Problem, a new synthesis problem adapted specifically for supporting iterative specification refinement in order to find a particular target solution. In contrast to prior work, we prove that synthesizers that solve the Programming by Navigation Synthesis Problem show all valid next steps ( Strong Completeness ) and only valid next steps ( Strong Soundness ). To meet the demands of the Programming by Navigation Synthesis Problem, we introduce an algorithm to turn a type inhabitation oracle (in the style of classical logic) into a fully constructive program synthesizer.We then define such an oracle via sound compilation to Datalog. Our empirical evaluation shows that this technique results in an efficient Programming by Navigation synthesizer that solves tasks that are either impossible or too large for baselines to solve. Our synthesizer is the first to guarantee that its specification refinement process satisfies both Strong Completeness and Strong Soundness .