We introduce APPL (Abstract Program Property Logic), a unifying Hoare-style logic that subsumes standard Hoare logic, incorrectness logic, and several variants of Hyper Hoare logic. APPL provides a principled foundation for abstract program logics parameterised by an abstract domain, encompassing both existing and novel abstractions of properties and hyperproperties. The logic is grounded in a semantic framework where the meaning of commands is first defined on a lattice basis and then extended to the full lattice via additivity. Crucially, nondeterministic choice is interpreted by a monoidal operator that need not be idempotent nor coincide with the lattice join. This flexibility allows the framework to capture collecting semantics, various classes of abstract semantics, and hypersemantics. The APPL proof system is sound, and it is relatively complete whenever the property language is sufficiently expressive. When the property language is restricted to an abstract domain, the result is a sound abstract deduction system based on best correct approximations. Relative completeness with respect to a corresponding abstract semantics is recovered provided the abstract domain is complete, in the sense of abstract interpretation, for the monoidal operator.

翻译：本文提出APPL（抽象程序属性逻辑），这是一种统一的霍尔风格逻辑，它涵盖了标准霍尔逻辑、不正确性逻辑以及多种超霍尔逻辑变体。APPL为以抽象域参数化的抽象程序逻辑提供了理论基础，涵盖了对属性和超属性的现有及新颖抽象。该逻辑建立在一个语义框架之上：首先在格基上定义命令的语义，然后通过可加性扩展至完整格。关键之处在于，非确定性选择由一个幺半群算子解释，该算子既不必满足幂等性，也不必与格并运算一致。这种灵活性使得该框架能够捕捉收集语义、各类抽象语义以及超语义。APPL证明系统是可靠的，并且在属性语言具有足够表达力时具备相对完备性。当属性语言被限制在某个抽象域时，所得结果是一个基于最佳正确近似的可靠抽象演绎系统。若该抽象域在抽象解释意义下对幺半群算子具有完备性，则可恢复相对于相应抽象语义的相对完备性。