霍尔三元组

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

这里的P和Q是断言而C是命令。P叫做前条件而Q叫做后条件。断言是谓词逻辑的公式。这个三元组在直觉上读做:只要P在C执行前的状态下成立，则在执行之后Q也成立。注意如果C不终止，也就没有"之后"了，所以Q在根本上可以是任何语句。实际上，你可以选择Q为假来表达C不终止。事实上，这种情形叫做"部分正确(partial correctness）"。如果C终止并且在终止时Q是真，则表达式被称作"全部正确性（total correctness）"。终止必须被单独证明。

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

部分正确性

空语句公理

如果P在一个空语句之前成立，那么在执行这个空语句之后也是成立的。 "skip"在这里表示空语句（Empty statement）。

赋值公理模式

赋值公理声称，关于对赋值右手端的变量的以前为真的任何命题在赋值之后仍然成立:

这里的P[E/x]{\displaystyle P[E/x]}指示表达式P中变量x的所有自由出现都被替代为表达式E。

有效的三元组的两个例子:

顺序规则

例如，考虑赋值公理的下列两个实例:

和

通过顺序规则，将得到:

条件规则

While规则

这里的P是循环不变条件。

推论规则

全部正确性

上述规则只证明部分正确性。可以通过扩展版本的While规则证明全部正确性。

全部正确性的While规则:

在本文中，除了维持循环不变条件，还能通过其值在每次重复期间递减的项就是这里的t的方式来证明终止。注意t必须从良定集合中取值，所以循环的每一步都通过递减有限链的成员来计数。

参见

契约式设计

动态逻辑

艾兹赫尔·戴克斯特拉

谓词变换者语义

程序验证

参考文献

来源

C. A. R. Hoare. "An axiomatic basis for computer programming". Communications of the ACM, 12(10):576–585, October 1969.doi:10.1145/363235.363259

Robert D. Tennent: "Specifying Software" (a recent textbook that includes an introduction to Hoare logic) ISBN 0-521-00401-2[1]

免责声明：以上内容版权归原作者所有，如有侵犯您的原创版权请告知，我们将尽快删除相关内容。感谢每一位辛勤著写的作者，感谢每一位的分享。