论文部分内容阅读
本文对程序验证中涉及到的Hoare逻辑，分离逻辑和模型检测进行了研究。 Hoare逻辑是程序验证中的根本方法。我们研究了Peano算术理论下的Hoare逻辑的完备性问题，在以下三方面做出了创新性的贡献。 (1)提出了Hoare逻辑在非标准模型上的一种具体的公理语义，证明了Hoare逻辑相对于该语义是逻辑完备的。 (2)给出了Hoare逻辑在输入限制为标准数下的逻辑完备的极小条件。 (3)给出了Hoare逻辑在前后断言限制在算术公式的子集下相对于标准模型完备的充要条件。 作为Hoare逻辑的一种重要扩展，分离逻辑能够对包含堆和栈等动态数据结构的程序进行推理。我们研究了带有归纳定义的组合树谓词和数据约束的分离逻辑的可满足性问题:论证了一个关于AVL组合树谓词数据约束的最小不动点在Presburger算术语言下的自然数模型上的不可表示性;给出了一类组合树谓词数据约束的最小不动点求解算法;给出了一个包含该类组合树谓词的分离逻辑可满足性判定的完备算法。 模型检测是形式验证在实际使用中最成功的方法之一。我们研究了关于ACTL时序逻辑的限界模型检测算法的优化问题:改进了具有线性见证的ECTL公式（与具有线性反例的ACTL公式对偶）的限界语义;应用该语义降低了一类ACTL公式的检测算法复杂度。