This paper introduces a dynamic logic extension of separation logic. The assertion language of separation logic is extended with modalities for the five types of the basic instructions of separation logic: simple assignment, look-up, mutation, allocation, and de-allocation. The main novelty of the resulting dynamic logic is that it allows to combine different approaches to resolving these modalities. One such approach is based on the standard weakest precondition calculus of separation logic. The other approach introduced in this paper provides a novel alternative formalization in the proposed dynamic logic extension of separation logic. The soundness and completeness of this axiomatization has been formalized in the Coq theorem prover.

翻译：本文提出了一种分离逻辑的动态逻辑扩展。该扩展在分离逻辑断言语言的基础上，引入了针对分离逻辑五类基本指令（简单赋值、查值、修改、分配与释放）的模态算子。这一动态逻辑的核心创新在于允许通过不同方法解析这些模态算子。其中一种方法基于标准分离逻辑的最弱前置条件演算，而本文提出的另一种方法则在所构建的动态逻辑扩展框架中，创新性地给出了形式化替代方案。该公理化的可靠性与完备性已在Coq定理证明器中完成形式化验证。