关于断言语言中引入逻辑变量的研究

摘要 基于Hoare逻辑推理规则去验证程序安全性的研究是程序验证领域的重要发展方向.但是在Hoare逻辑中，仅依靠程序变量的断言语言无法表达程序上下文中不变性质.本文研究通过在断言语言中引入逻辑变量的方式来表达程序上下文不变性质，同时详细介绍了引入逻辑变量带来的问题以及给出解决问题的途径，最后以带逻辑变量的平衡二叉树插入程序为例展示了引入逻辑变量的作用