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（抽象程序性质逻辑），这是一种统一的Hoare风格逻辑，涵盖了标准Hoare逻辑、不正确性逻辑及Hyper Hoare逻辑的多种变体。APPL为以抽象域为参数的抽象程序逻辑提供了理论基础，既包含现有也包含新颖的性质与超性质抽象形式。该逻辑建立于语义框架之上：命令的含义首先在格基上定义，再通过可加性扩展至全格。关键在于，非确定性选择通过一个无需幂等也不一定与格并运算一致的幺半群算子进行解释。这种灵活性使得框架能够捕捉收集语义、各类抽象语义以及超语义。APPL证明系统是可靠的，且当性质语言足够表达时是相对完备的。当性质语言限制为抽象域时，所得结果基于最优正确近似构成一个可靠的抽象演绎系统。只要抽象域对于幺半群算子在抽象解释意义下是完备的，即可恢复相对于对应抽象语义的相对完备性。