证明正规程序的正确性与完备性——一种声明式方法

我们主张采用声明式方法来证明逻辑程序的性质。全面正确性可分为正确性、完备性和整洁终止；后者包括非失败。只有整洁终止依赖于操作语义，特别是选择规则。我们展示了如何以声明式方式处理正确性和完备性，仅从逻辑角度对待程序。此方法使用的规范是解释（或理论）。我们指出，正确性的规范可能不同于完备性的规范，因为通常存在既不被视为错误也不被要求计算的答案。我们给出了确定性程序的正确性和完备性证明方法，并将其推广到正规程序。对于正规程序，我们使用三值完备语义；这是对应于有限失败否定的标准语义。证明方法仅使用经典二值逻辑。我们使用三值完备语义的二值刻画，这可能具有独立的意义。所提出的方法与基于操作语义的方法进行了比较。我们还利用本文的思想推广了一种证明正规程序终止的已知方法。