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.
翻译:局部完整性逻辑( LLLL) 已被作为程序逻辑, 用以证明程序规格的正确性和不正确性。 LCL 是一种抽象逻辑, 由抽象的域参数进行参数化, 能够将程序行为的超常和偏差结合起来。 事实证明, LCL 即刻化为微小的单吨抽象现象, 归结为 O' Hearn 不正确的逻辑, 使我们能够证明程序错误的存在。 最近已经证明, Kleene 代数与测试( KAT) 的合适扩展, 可以在同一方程框架内代表 O' Hearn 不正确性和 Hoare 正确性程序逻辑。 在这项工作中, 我们通过显示 KAT 是如何与模式钻石操作者或顶端元素一起扩展的来代表本地完整性逻辑 LCLCL。 这是通过研究这些扩展的KAT 如何赋予一个抽象域来达到的, 从而确定正确性/ 不正确性 LCLCL 3 的有效性, 并显示 LCLC 证据系统在某种假设下是逻辑正确性和完整的。