Hoare logics are proof systems that allow one to formally establish properties of computer programs. Traditional Hoare logics prove properties of individual program executions (so-called trace properties, such as functional correctness). Hoare logic has been generalized to prove also properties of multiple executions of a program (so-called hyperproperties, such as determinism or non-interference). These program logics prove the absence of (bad combinations of) executions. On the other hand, program logics similar to Hoare logic have been proposed to disprove program properties (e.g., Incorrectness Logic), by proving the existence of (bad combinations of) executions. All of these logics have in common that they specify program properties using assertions over a fixed number of states, for instance, a single pre- and post-state for functional properties or pairs of pre- and post-states for non-interference. In this paper, we present Hyper Hoare Logic, a generalization of Hoare logic that lifts assertions to properties of arbitrary sets of states. The resulting logic is simple yet expressive: its judgments can express arbitrary trace- and hyperproperties over the terminating executions of a program. By allowing assertions to reason about sets of states, Hyper Hoare Logic can reason about both the absence and the existence of (combinations of) executions, and, thereby, supports both proving and disproving program (hyper-)properties within the same logic. In fact, we prove that Hyper Hoare Logic subsumes the properties handled by numerous existing correctness and incorrectness logics, and can express hyperproperties that no existing Hoare logic can. We also prove that Hyper Hoare Logic is sound and complete, and admits powerful compositionality rules. All our technical results have been proved in Isabelle/HOL.

翻译：霍尔逻辑是一种能够严格建立计算机程序性质的证明系统。传统的霍尔逻辑可证明单个程序执行的性质（即所谓的迹性质，例如功能正确性）。霍尔逻辑已被推广用于证明一个程序的多次执行的性质（即所谓的超性质，例如确定性和非干扰性）。这些程序逻辑用于证明不存在（不良的执行组合）。另一方面，类似于霍尔逻辑的程序逻辑已被提出用于证伪程序性质（例如不正确性逻辑），其通过证明存在（不良的执行组合）来实现。所有这些逻辑的共同点在于，它们使用基于固定数量状态的断言来指定程序性质，例如功能性质中的单个前置状态和后置状态，或非干扰性中的前置状态对和后置状态对。在本文中，我们提出了超霍尔逻辑，这是对霍尔逻辑的一种推广，它将断言提升到任意状态集合的性质。由此得到的逻辑既简单又富有表现力：其判断可以表达程序终止执行上的任意迹性质和超性质。通过允许断言推理状态集合，超霍尔逻辑能够同时推理（执行组合的）不存在性和存在性，从而在同一逻辑内支持程序（超）性质的证明与证伪。事实上，我们证明了超霍尔逻辑涵盖了众多现有正确性逻辑和不正确性逻辑所处理的性质，并能表达任何现有霍尔逻辑无法表达的超性质。我们还证明了超霍尔逻辑是可靠且完备的，并拥有强大的组合性规则。所有我们的技术结果均在Isabelle/HOL中得到验证。