Dynamic Separation Logic

TL;DR

This paper introduces a dynamic logic extension of separation logic that allows to combine different approaches to resolving these modalities for simple assignment, look-up, mutation, allocation, and de-allocation.

Abstract

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.

Figures (6)

• Figure 1: Semantics of basic instructions of heap manipulating programs.
• Figure 2: Semantics of Dynamic Separation Logic.
• Figure 3: Strongest postcondition axioms of separation logic (SP-DSL), where $y$ is fresh everywhere and $x$ does not occur in $e$ in case of $x:=\hbox{\bf cons}(e)$.
• Figure 4: Syntax and semantics of heap manipulating programs.
• Figure 5: Hoare's standard proof rules.

Theorems & Definitions (14)

• lemma 1: Basic equivalences
• lemma 2: Substitution lemma
• proof
• lemma 3: Axioms basic instructions
• lemma 4: Heap update
• lemma 5: Heap clear
• proof
• theorem 1: Completeness of E
• theorem 2: Completeness local mutation axiom
• proof