我好像已经把你搞糊涂了…… 我们先来科普一下 Hoare Logic。
Hoare Logic（https://en.wikipedia.org/wiki/Hoare_logic） 是一种形式验证的方法，用于验证程序的正确性。它的做法是，先给代码标注一些“前条件”和“后条件”（pre-condition 和 post-condition），然后就可以进行逻辑推理，验证代码的某些基本属性，比如转账之后余额是正确的。
举一个很简单的 Hoare Logic 例子：
{x=0} x:=x+1 {x>0}
它的意思是，如果开头 x 等于 0，那么 x:=x+1 执行之后，x 应该大于 0。这里的前条件（pre-condition）是 x=0，后条件（post-condition）是 x > 0。如果 x 开头是零，执行 x:=x+1 之后，x 就会大于 0，所以这句代码就验证通过了。
Hoare Logic 的系统把所有这些前后条件和代码串接起来，经过逻辑推导验证，就可以作出这样的保证：在前条件满足的情况下，执行代码之后，后条件一定是成立的。如果所有这些条件都满足，系统就认为这是“正确的程序”。注意这里的所谓“正确”，完全是由人来决定的，系统并不知道“正确”是什么意思。
Hoare Logic 对于程序的安全性，确实可以起到一定的效果，它已经被应用到了一些实际的项目。比如微软 Windows 的驱动程序代码里面，有一种“安全标注语言”，叫做 SAL，其实就是 Hoare Logic 的一个实现。然而前条件和后条件是什么，你必须自己给代码加上标注，否则系统就不能工作。
比如上面的例子，系统如何知道我想要“x>0”这个性质呢？只有我自己把它写出来。所以要使用 Hoare Logic，必须在代码上标注很多的 pre-condtion 和 post-condition。这些条件要如何写，必须要深入理解程序语言和形式逻辑的原理。这个工作需要经过严格训练的专家来完成，而且需要很多的时间。
版权申明：本内容来自于互联网，属第三方汇集推荐平台。本文的版权归原作者所有，文章言论不代表链门户的观点，链门户不承担任何法律责任。如有侵权请联系QQ：3341927519进行反馈。
