程序验证

  在程序验证中，对霍尔三元组的引入也较《Software Foundation》更加自然易懂。该章节的证明过程也与VST中提供的方法类似。

  本章使用的方法是基于证明的，半自动的，面向性质的。因为当程序可以操作非平凡的数据如整数、表或树的变量时，就进入了无限状态空间。模型检测将不再适用。

软件验证的一种框架

  产生软件的框架可以是：

• 将应用领域中需求的非形式描述R转化成某种符号逻辑中“等价的”公式$\phi_R$；
• 编写能实现$\phi_R$的程序P；
• 证明程序P满足公式$\phi_R$。

  霍尔三元组是为了更加形式化的描述需求而产生的一种语法，是规范的一种形式。霍尔三元组是霍尔逻辑的中心特征。在霍尔三元组中前置条件和后置条件是谓词逻辑中的公式。

  定义（部分正确性）　如果对满足$\phi$的所有状态，只要P实际终止，执行P后的结果状态就满足后置条件$\psi$，我们说三元组($|\phi|$)P($|\psi|$)在部分正确意义下满足。此时，关系$\models_{\text{par}}$($|\phi|$)P($|\psi|$)成立。我们称$\models_{\text{par}}$为部分正确性的满足关系。

  定义（完全正确性）　我们说三元组($|\phi|$)P($|\psi|$)在完全正确意义下满足，如果在满足前置条件$\phi$的所有状态下执行程序P，P肯定终止，而且结果状态满足后置条件$\psi$。此时，我们说关系$\models_{\text{tot}}$($|\phi|$)P($|\psi|$)成立。我们称$\models_{\text{tot}}$为完全正确性的满足关系。

  证明完全正确性通常可由先证明部分正确性、然后证明可终止。

• 程序变量：在待验证的程序中的变量称为程序变量；
• 逻辑变量：只出现在构成前置条件和后置条件的逻辑公式中，而不出现在待验证的代码中。

部分正确性的证明演算

  证明规则如下：