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定理证明器中得到形式化验证。