什么是程序逻辑？

程序逻辑是描述和论证程序行为的逻辑，又称霍尔逻辑。程序和逻辑有着本质的联系。如果把程序看成一个执行过程，程序逻辑的基本方法是先给出建立程序和逻辑间联系的形式化方法，然后建立程序逻辑系统，并在此系统中研究程序的各种性质。

简介：

Hoare 逻辑(也叫做Floyd–Hoare 逻辑)是英国计算机科学家C. A. R. Hoare开发的形式系统，随后为 Hoare 和其他研究者所精制。它发表于 Hoare 1969年的论文"计算机程序的公理基础"中。这个系统的用途是为了使用严格的数理逻辑推理计算机程序的正确性提供一组逻辑规则。

Hoare 认可 Robert Floyd的早期贡献，他为流程图提供了类似的系统。

Hoare 逻辑的中心特征是Hoare 三元组。这种三元组描述一段代码的执行如何改变计算的状态。Hoare 三元组有如下形式

{P}C{Q}这里的 P 和 Q 是断言而 C 是命令。P 叫做前条件而 Q 叫做后条件。断言是谓词逻辑的公式。这个三元组在直觉上读做: 只要 P 在 C 执行前的状态下成立，则在执行之后 Q 也成立。注意如果 C 不终止，也就没有"之后"了，所以 Q 在根本上可以是任何语句。实际上，你可以选择 Q 为假来表达 C 不终止。

这叫做"部分正确"的。如果 C 终止并且在终止时 Q 是真，则表达式就是"全部正确"的。终止必须被单独证明。

Hoare 逻辑为简单的命令式编程语言的所有构造提供了公理和推理规则。除了给 Hoare 论文中的简单语言的规则，其他语言构造的规则也已经被 Hoare 和很多其他研究者开发出来了。包括并发、过程、goto语句，和指针。

这个逻辑表达式，可以化简，就是：Q = XYZ + XYF + XZF

假设，各个变量对应的引脚如下：

X: P1.0

Y: P1.1

Z: P1.2

F: P1.3

Q: P1.7

程序如下：

MOV C, P1.0

ANL C, P1.1

ANL C, P1.2

MOV F0, C

MOV C, P1.0

ANL C, P1.1

ANL C, P1.3

ORL C, F0

MOV F0, C

MOV C, P1.0

ANL C, P1.2

ANL C, P1.3

ORL C, F0

MOV P1.7, C

END

---