论文标题
测试的局部完整性逻辑
Local Completeness Logic on Kleene Algebra with Tests
论文作者
论文摘要
本地完整性逻辑（LCL）已作为程序逻辑提出，以证明程序规范的正确性和错误性。 LCL是一种抽象逻辑，通过一个抽象域进行了参数化，该域允许将程序行为的过度和不足的磁化结合起来。事实证明，LCL实例化为琐碎的单例抽象，归结为O'Hearn Inforcectness逻辑，这使我们能够证明程序错误的存在。最近证明，具有测试（KAT）的Kleene代数的合适扩展允许在相同的方程框架内代表O'Hearn不正确性和Hoare正确性程序逻辑。在这项工作中，我们通过显示Kats如何使用模态钻石操作员或顶部元素来代表局部完整性逻辑LCL来概括此结果。这是通过研究如何将这些扩展的Kats赋予抽象域以定义正确性/不正确性LCL三元组的有效性并表明LCL证明系统在逻辑上是合理的，并且在某些假设完整的情况下实现。
Local Completeness Logic (LCL) has been put forward as a program logic for proving both the correctness and incorrectness of program specifications. LCL is an abstract logic, parameterized by an abstract domain that allows combining over- and under-approximations of program behaviors. It turns out that LCL instantiated to the trivial singleton abstraction boils down to O'Hearn incorrectness logic, which allows us to prove the presence of program bugs. It has been recently proved that suitable extensions of Kleene algebra with tests (KAT) allow representing both O'Hearn incorrectness and Hoare correctness program logics within the same equational framework. In this work, we generalize this result by showing how KATs extended either with a modal diamond operator or with a top element are able to represent the local completeness logic LCL. This is achieved by studying how these extended KATs can be endowed with an abstract domain so as to define the validity of correctness/incorrectness LCL triples and to show that the LCL proof system is logically sound and, under some hypotheses, complete.
