C语言子集C Certified上的程序逻辑与可靠性证明

"一个C语言子集上的程序逻辑.pdf" 这篇学术论文主要探讨的是在C语言的一个子集，称为C Certified (CCode Certified)，上的程序逻辑设计。作者是王勇朝、李兆鹏和冯新宇，来自中国科学技术大学计算机科学与技术学院以及中国科学技术大学苏州研究院软件安全实验室。该研究基于分离逻辑和C语言的标准规范，构建了一种用于程序验证的逻辑体系，旨在提高代码的可靠性并简化验证过程。 操作语义是这个程序逻辑的核心部分，它采用了小步执行的模型。小步语义将程序的执行分解为一系列微小的步骤，这样可以更细致地分析并发程序的行为，同时也为未来对并发程序的验证提供了扩展的基础。 推导规则采用扩展的Hoare三元组形式，这是程序验证中的一个常见方法，用于描述程序的前条件、后条件以及程序的执行。扩展的Hoare三元组允许涵盖更多C语言的特性，如指针、结构体等，使得逻辑能够适用于更广泛的C语言程序。 在可靠性证明方面，文章采用直接定义法在语义层面上定义推导规则。这种直接定义法是形式化验证中广泛接受的方法，确保了逻辑的正确性和可信度。为了进一步增强逻辑的可信度，作者还在Coq证明助手环境下实现了可靠性证明，并提供了一个可以通过机器自动检查的证明，这极大地提高了证明的可信度和有效性。 论文还通过实际的证明实例展示了所提出的程序逻辑的实用性。这些实例证明了该逻辑如何简化了程序验证工具的工作，使得验证过程更加高效。关键词包括C语言、小步语义、程序逻辑、可靠性以及形式化验证，这些关键词突出了研究的主要关注点和贡献。 这篇论文为C语言的程序验证提供了一个新的工具和方法，通过对C语言子集的特定逻辑设计，使得代码的验证更加精确和自动化，对于提升软件质量和安全性具有重要意义。