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

P →[S]Q

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

P →Q

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

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

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

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

P →□(STOP →Q)

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

P →◇(STOP&Q)

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