超级霍尔逻辑：（非）证明程序的超属性（扩展版本）
摘要：超级Hoare逻辑的介绍及其在计算机程序中建立性质的能力。这种逻辑不仅能证明单个程序执行的性质（如功能正确性），还能证明程序多次执行的性质（如确定性或非干扰性）。超级Hoare逻辑也可以证明（不良组合的）程序执行的缺失。另一方面，类似Hoare逻辑的程序逻辑也可以证明程序性质的不正确性（如不正确逻辑），通过证明（不良组合的）执行的存在。所有这些逻辑的共同之处在于使用断言指定程序属性，这些属性涉及一定数量的状态，例如，功能性属性的单个前后状态或非干扰性的前后状态对。本文介绍了超级Hoare逻辑，这是Hoare逻辑的一种推广形式，将断言升级为任意状态集合的属性。所得逻辑简单而富有表达力：其判断可以表达程序终止执行的任意跟踪和超本质属性。通过允许断言对状态集合进行推理，超级Hoare逻辑可以同时对（组合的）程序执行的缺失和存在进行推理，并因此在同一逻辑中支持程序（超级）属性的证明和反证。实际上，我们证明了超级Hoare逻辑涵盖了许多现有正确性和错误性逻辑处理的属性，并可以表达没有现有Hoare逻辑可以表达的超本质属性。我们还证明超级Hoare逻辑是完备和完全的，并接受强大的可组合性规则。我们所有的技术结果都在Isabelle/HOL中得到了证明。
作者：Thibault Dardinier, Peter M"uller
论文ID：2301.10037
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-25