Following Hoare's seminal invention, now called Hoare logic, to reason about correctness of computer programs, we advocate a related but fundamentally different approach to reason about access security of computer programs such as access control. We define the formalism, which we denote access Hoare logic, and present examples which demonstrate its usefulness and fundamental difference to Hoare logic. We prove soundness and completeness of access Hoare logic, and provide a link between access Hoare logic and standard Hoare logic. We also demonstrate a fundamental difference of access Hoare logic to other approaches, in particular incorrectness logic.

翻译：继霍尔开创性地提出如今称为霍尔逻辑的方法以推理计算机程序的正确性之后，我们倡导一种相关但根本不同的方法来推理计算机程序的访问安全性，例如访问控制。我们定义了这一形式化体系，称之为访问霍尔逻辑，并通过实例展示其有效性及其与霍尔逻辑的根本区别。我们证明了访问霍尔逻辑的可靠性和完备性，并在访问霍尔逻辑与标准霍尔逻辑之间建立了联系。我们还展示了访问霍尔逻辑与其他方法（特别是不正确性逻辑）的根本区别。