论文标题
一个不现有的关系逻辑：不安全感的预示逻辑，不正确的实施及更多
An Under-Approximate Relational Logic: Heralding Logics of Insecurity, Incorrect Implementation & More
论文作者
论文摘要
最近，作者提出了针对程序的理解较低的逻辑。到目前为止，所有这些逻辑都局限于有关个人程序行为的推理。然而，存在许多过分的关系逻辑，用于推理成对的程序并关联其行为。我们为简单的命令式语言IMP提供了第一个不异型的关系逻辑。我们证明我们的逻辑既声音又完整。此外，我们还展示了如何将这种逻辑中的推理分解为较低的Hoare逻辑中的非关系推理，从而反映了贝林格（Beringer）的结果过度同一性的关系逻辑。我们说明了逻辑在一些小例子上的应用，在这些例子中我们证明了不安全感的存在。
Recently, authors have proposed under-approximate logics for reasoning about programs. So far, all such logics have been confined to reasoning about individual program behaviours. Yet there exist many over-approximate relational logics for reasoning about pairs of programs and relating their behaviours. We present the first under-approximate relational logic, for the simple imperative language IMP. We prove our logic is both sound and complete. Additionally, we show how reasoning in this logic can be decomposed into non-relational reasoning in an under-approximate Hoare logic, mirroring Beringer's result for over-approximate relational logics. We illustrate the application of our logic on some small examples in which we provably demonstrate the presence of insecurity.
