Partial correctness of imperative or functional programming divides in logic programming into two notions. Correctness means that all answers of the program are compatible with the specification. Completeness means that the program produces all the answers required by the specifications. We also consider semi-completeness -- completeness for those queries for which the program does not diverge. This paper presents an approach to systematically construct provably correct and semi-complete logic programs, for a given specification. Normal programs are considered, under Kunen's 3-valued completion semantics (of negation as finite failure) and the well-founded semantics (of negation as possibly infinite failure). The approach is declarative, it abstracts from details of operational semantics, like e.g.\ the form of the selected literals (``procedure calls'') during the computation. The proposed method is simple, and can be used (maybe informally) in actual everyday programming.

翻译：在逻辑编程中，命令式或函数式编程的部分正确性概念被划分为两个部分。正确性意味着程序的所有答案均与规范兼容。完备性意味着程序能产生规范所要求的所有答案。我们还考虑了半完备性——即对于程序不发散的那些查询而言的完备性。本文提出了一种方法，用于针对给定规范，系统化地构建可证明正确且半完备的逻辑程序。所考虑的是在Kunen的三值完成语义（将否定视为有限失败）和良基语义（将否定视为可能无限失败）下的正规程序。该方法具有声明性，它抽象了操作语义的细节，例如计算过程中被选文字（“过程调用”）的形式。所提出的方法简单明了，并且可以（或许非正式地）用于实际的日常编程中。