逻辑程序的加细演算
A Refinement Calculus for Logic Programs
摘要：
现有的精化演算提供了从规范逐步开发命令式程序的框架。本文提出了一种用于推导逻辑程序的精化演算。演算包含一个广谱逻辑程序设计语言，包括可执行结构，如顺序合取、析取和存在量化，以及规范结构，如一般谓词、假设和泛量化。一个声明性的语义定义为这个广谱语言的执行的基础上。执行是从状态到状态的部分函数，其中状态表示为一组绑定。语义用于定义程序和规范的含义，包括参数和递归。为了完成演算，在广谱语言的程序的正确性保持求精的概念被定义和细化法律开发程序的介绍。精化演算说明使用示例推导和原型工具支持进行了讨论。
英文摘要：
Existing refinement calculi provide frameworks for the stepwise development of imperative programs from specifications. This paper presents a refinement calculus for deriving logic programs. The calculus contains a wide-spectrum logic programming language, including executable constructs such as sequential conjunction, disjunction, and existential quantification, as well as specification constructs such as general predicates, assumptions and universal quantification. A declarative semantics is defined for this wide-spectrum language based on executions. Executions are partial functions from states to states, where a state is represented as a set of bindings. The semantics is used to define the meaning of programs and specifications, including parameters and recursion. To complete the calculus, a notion of correctness-preserving refinement over programs in the wide-spectrum language is defined and refinement laws for developing programs are introduced. The refinement calculus is illustrated using example derivations and prototype tool support is discussed.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
