作者：李为胜; 罗奇鸣; 陈意云hoare逻辑形式化验证逻辑变量断言语言
摘要：基于Hoare逻辑推理规则去验证程序安全性的研究是程序验证领域的重要发展方向．但是在Hoare逻辑中，仅依靠程序变量的断言语言无法表达程序上下文中不变性质．本文研究通过在断言语言中引入逻辑变量的方式来表达程序上下文不变性质，同时详细介绍了引入逻辑变量带来的问题以及给出解决问题的途径，最后以带逻辑变量的平衡二叉树插入程序为例展示了引入逻辑变量的作用．
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
《小型微型计算机系统》（CN：21-1106/TP）是一本有较高学术价值的大型月刊，自创刊以来，选题新奇而不失报道广度，服务大众而不失理论高度。颇受业界和广大读者的关注和好评。 《小型微型计算机系统》杂志刊登文章的内容涵盖计算技术的各个领域(计算数学除外)。包括计算机科学理论、体系结构、计算机软件、数据库、网络与通讯、人工智能、多媒体、计算机图形与图像、算法理论研究等各方面的学术论文。
部级期刊
人气 230156 评论 65
人气 214635 评论 35
省级期刊
人气 213005 评论 71
北大期刊、统计源期刊
人气 193043 评论 73
