[拼音]：chengxu luoji

[外文]：program logic

描述和论证程序行为的逻辑，又称霍尔逻辑。程序和逻辑有着本质的联系。如果把程序看成一个执行过程，它接收一些信息，又输出一些信息。用逻辑公式描述对输入和输出信息的要求，就可以建立逻辑公式和程序间的联系，表示为

｛P｝S｛Q｝

其中P和Q为有关程序变元的逻辑表达式；P称为S的前置条件；Q称为S的后置条件。此公式表示:如果程序S执行前程序变量的值满足前置条件P，且程序S终止，则程序S执行终止后，程序变量的值满足后置条件Q。如果进一步建立一套关于这类公式的推理规则，就能得到一个描述程序行为的逻辑系统，可以在此系统中研究程序的性质，这就是程序逻辑。

程序是在机器中执行的，程序中每个语句的执行导致机器状态的变化，因此程序的执行又可以由机器状态变化的序列表达。数理逻辑中的模态逻辑正是描述动态变元变化的一种逻辑，因此以模态逻辑为基础也可揭示逻辑与程序间的深刻联系。

美国R.W.弗洛依德于60年代中期把框图程序对应为逻辑公式，提出使用逻辑描述和分析程序的想法。1969年前后英国C.A.R.霍尔首次给出一类程序语言的逻辑系统，提出程序部分正确性的形式验证规则（见程序验证）。70年代初，波兰和瑞士一些学者提出使用算法逻辑描述和分析程序，这是第一次把模态逻辑引入程序逻辑的尝试。70年代中期，有些科学家进一步提出使用动态逻辑和时态逻辑，描述和论证程序，推动了程序逻辑的研究。

程序逻辑的基本方法是先给出建立程序和逻辑间联系的形式化方法，然后建立程序逻辑系统，并在此系统中研究程序的各种性质，例如，在霍尔逻辑中，程序逻辑公式的形式为

｛P｝S｛Q｝

如上所述，这类公式不能表示S的终止特性，因此霍尔逻辑是讨论程序部分正确性的逻辑。如果在霍尔逻辑系统中可以证明｛P｝S｛Q｝，同时又能证明对满足前置条件的所有输入变量程序S都终止，则称程序具有完全正确性。

在公式｛P｝S｛Q｝中逻辑表达式P和Q实际上只是当作语句S的注释使用的，对逻辑公式｛P｝S｛Q｝不能进行逻辑运算，例如蕴含公式｛P₁｝S₁｛Q₁｝→｛P₂｝S₂｛Q₂｝就没有意义，因此霍尔逻辑还没有彻底把程序和逻辑统一起来。解决的方法之一就是使用动态逻辑，它是一种模态逻辑。在动态逻辑中除了通常的命题连接词 墯，∨，∧，→及作用于非动态变元的量词和凬外，还可以引入动态连接词，例如[ ]，[S]Q表示当S 终止时Q为真。这样墯[S]Q，[S₁]P→[S₂]Q等就都是有意义的逻辑公式，如果进一步令〈 〉表示墯[ ]墯，则<S>Q表示存在一个时刻S终止且Q为真。程序S的部分正确性问题就可以表示为

P →[S]Q

即P真蕴含当S终止时Q为真。如果S是确定性语句，则其完全正确性问题可以表示为

P →<S>Q

即P真蕴含S在某一时刻终止且Q真。

霍尔逻辑的基本思想是用逻辑描述程序的执行结果，与之对应的另一种方法是用逻辑刻画程序的全部行为，即把程序的执行过程看成机器状态的一个变化序列。自70年代中期，并发式程序设计逐渐成为程序理论的重要课题后，这种观点就显得十分必要，因为刻画在程序执行过程中，各任务之间的同步和信息交换常常是不可少的。时态逻辑是关于随着时间而不断改变其值的动态变元（叫作时序变元）的一种模态逻辑。因此它自然地被引入到程序逻辑中。时态逻辑以当前时间为基本出发点，除使用常用逻辑连接词及作用于非时序变元的量词外，还可以用引入时态连接词的办法刻画更复杂的动态性质。例如，可以引入连接词◇及□：

◇P 表示在将来某一时刻P真，

□P 表示P从此以后永真。使用时态逻辑可以对每个程序构造出它所对应的一个逻辑系统，并可以在此系统中刻画终止（记作STOP）及无死锁等概念。而程序S 的部分正确性问题就可以表示为

P →□(STOP →Q)

在程序S 所对应的逻辑系统中成立，即程序开始执行时P真蕴含如果将来任一时刻程序终止则Q真，而其完全正确性则可表示为

P →◇(STOP&Q)

在该逻辑系统中成立，即程序开始执行时P真蕴含存在某一时刻S 终止并且Q真。

由于程序逻辑使用逻辑系统描述程序的行为，它与具体执行程序的机器无关，因此程序逻辑的研究为公理语义学提供了理论基础。在逻辑系统中又可以分析和论证程序的性质，因此它又是程序验证的理论基础。

现代软件工程的一个重要方法是在程序设计之前，必须把程序要达到的目标即功能描述交待清楚。功能描述应当简洁明瞭，而不必关心执行细节，因此可以使用逻辑语言的全部公式。

程序设计的任务就是编制程序使其满足描述。程序逻辑的研究表明，程序和逻辑都可以作为逻辑系统的逻辑公式，所不同的是程序只出现在一部分特定的逻辑公式中。因此设计程序使之满足描述的过程，从逻辑演算角度看，就是如何将表示功能描述的逻辑公式转化成表示程序的逻辑公式问题，因此程序逻辑的研究又为软件工程中自动化设计提供了有力工具。