霍尔逻辑

易经学习

天地变化的道理

分类目录

使用率很高网站

文章列表

生活要常常分享

维基百科

您身边百科全书

霍尔逻辑

点击查看词条快照

霍尔逻辑（），又称弗洛伊德-霍尔逻辑（-- ），是英国计算机科学家东尼·霍尔开发的形式系统，这个系统的用途是为了使用严格的数理逻辑推理来替计算机程序的正确性提供一组逻辑规则。这个想法起源于罗伯特·弗洛伊德于较早的研究，他为流程图提供了类似的系统。东尼·霍尔于1969年首次发表，随后为其他研究者所精制。霍尔三元组. 霍尔逻辑的中心特征是霍尔三元组（Hoare triple）。这种三元组描述一段代码的执行如何改变计算的状态。Hoare三元组有如下形式 formula_1 这里的 "P" 和 "Q" 是断言而 "C" 是命令。"P" 叫做前条件而 "Q" 叫做后条件。断言是谓词逻辑的公式。这个三元组在直觉上读做：只要 "P" 在 "C" 执行前的状态下成立，则在执行之后 "Q" 也成立。注意如果 "C" 不终止，也就没有"之后"了，所以 "Q" 在根本上可以是任何语句。实际上，你可以选择 "Q" 为假来表达 "C" 不终止。事实上，这种情形叫做 "部分正确（partial correctness）"。如果 "C" 终止并且在终止时 "Q" 是真，则表达式被称作 "全部正确性（total correctness）"。终止必须被单独证明。霍尔逻辑为简单的指令式编程语言的所有构造提供了公理和推理规则。除了给Hoare论文中的简单语言的规则，其他语言构造的规则也已经被Hoare和很多其他研究者开发完成。包括并发、过程、分支语句，和指针。 formula_2 部分正确性. 空语句公理. 如果P在一个空语句之前成立，那么在执行这个空语句之后也是成立的。 "skip"在这里表示空语句（Empty statement）。赋值公理模式. 赋值公理声称，关于对赋值右手端的变量的以前为真的任何命题在赋值之后仍然成立: formula_3 这里的formula_4指示表达式"P"中所有的自由变量"x"都被替代为表达式"E"。有效的三元组的两个例子: formula_5 formula_6 formula_7 顺序规则. 例如，考虑赋值公理的下列两个实例: formula_8 和 formula_9 通过顺序规则，将得到: formula_10 formula_11 formula_12 While规则. 这里的"P"是循环不变条件。 formula_13 全部正确性. 上述规则只证明部分正确性。可以通过扩展版本的While规则证明全部正确性。 formula_14 在本文中，除了维持循环不变条件，还能通过其值在每次重复期间递减的项就是这里的"t"的方式来证明终止。注意"t"必须从良定集合中取值，所以循环的每一步都通过递减有限链的成员来计数。

美国国防部长

余慕云

普维敦斯灰

洪山区

广辉电子

广达电脑

广达集团

穆斯塔法一世

伊豆大岛

香港房屋协会

盖德·穆勒

南华中学