# Dynamic Separation Logic

Frank S. de Boer  Hans-Dieter A. Hiep  Stijn de Gouw  Leiden Institute for
Advanced Computer Science (LIACS)
Leiden University
Leiden, the Netherlands  Computer Security group
Centrum Wiskunde & Informatica (CWI)
Amsterdam, the Netherlands  Department of Computer Science
Open University (OU)
Heerlen, the Netherlands

###### 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.

###### keywords:

Separation logic, dynamic logic, weakest precondition, sequential programs.

††volume: NN††journal: Electronic Notes in Theoretical Informatics and
Computer Science††volume: NN††thanks: Email<EMAIL_ADDRESS>Email:
<EMAIL_ADDRESS>Email<EMAIL_ADDRESS>
##  1 Introduction

This paper describes a study into the expressive power of separation logic
(SL, for short) with regard to the formalization of _weakest preconditions_
[7]. To this end, we introduce a novel dynamic logic extension of SL, which we
abbreviate by DSL (for Dynamic Separation Logic).

SL [19] extends Hoare logic for the specification and verification of heap
manipulating programs in terms of pre- and postconditions. The assertion
language of SL features the basic heap assertion $(x\mapsto e)$, ‘$x$ points
to $e$’, which expresses that the variable $x$ denotes the single allocated
memory location which stores the value of the expression $e$. The so-called
separating conjunction ($p\mathrel{*}q$) allows to split the heap, that is,
the set of allocated memory locations and their contents, into two disjoint
parts one of which satisfies the conjunct $p$ and the other satisfies $q$. The
separating implication $(p\mathrel{-\kern-1.99997pt*}{}q)$, roughly, holds if
every extension of the heap satisfies $q$, whenever $p$ holds for the
extension itself (separately). For an introduction to SL and an extensive
survey of the literature, intended for a broad audience, see the paper by A.
Charguéraud [5].

Dynamic logic [9] generalizes Hoare logics by introducing for each statement
of the underlying programming language a corresponding modality, so that the
formula $[S]p$ expresses the weakest precondition of the statement $S$ with
respect to the postcondition $p$. Informally, $[S]p$ is valid if every
terminating computation establishes $p$. In this paper we extend the assertion
language of SL with _modalities_ for the five types of the basic instructions
of SL: simple assignment, look-up, mutation, allocation, and de-allocation.
For any such basic instruction $S$, we then can introduce in the Hoare logic
the axiom

$\\{{[S]p}\\}\ {S}\ \\{{p}\\}$

which is trivially sound and complete by definition of $[S]p$. In case $S$ is
a simple assignment $x:=e$ and $p$ is an assertion in standard SL, we can
resolve the weakest precondition $[S]p$, as in first-order dynamic logic,
simply by _substituting_ every free occurrence of $x$ in $p$ by the expression
$e$.111After suitable renaming of the bound variables in $p$ such that no
variable of $e$ gets bound. In SL we can resolve $[S]p$, for any other basic
instruction $S$, by a formula with a hole $C_{S}(\cdot)$ in SL itself, such
that $C_{S}(p)$ is equivalent to $[S]p$. For example, the assertion

$(\exists y(x\mapsto y))*((x\mapsto e)\mathrel{-\kern-1.99997pt*}p)$

states that the heap can be split in a sub-heap which consists of a single
memory cell denoted by $x$ such that $p$ holds for every extension of the
other part with a single memory cell denoted by $x$ and which contains the
value of $e$. It follows that this assertion is equivalent to $[[x]:=e]p$,
where the _mutation_ instruction $[x]:=e$ assigns the value of the expression
$e$ to the heap location denoted by the variable $x$.

The main contribution of this paper is a complementary approach to resolving
$[S]p$, for any basic instruction. In this approach we obtain an alternative
characterization of the weakest precondition $[S]p$ by a novel axiomatization
of the modalities in DSL. This axiomatization allows for a characterization of
$[S]p$ _compositionally_ in terms of the syntactical structure of $p$.

O’Hearn, Reynolds, and Yang introduced local axioms [15] and show how to
derive from these local axioms a weakest precondition axiomatization of the
basic instructions in SL, using the frame rule and the separating implication
for expressing the weakest precondition. Yang [23] shows that the separating
implication is actually not needed to prove completeness of the local axioms
for simple assignments, look-up, allocation, and de-allocation. We illustrate
the expressiveness of DSL by extending this result to the local mutation
axiom. We further illustrate the expressiveness of DSL by a novel _strongest
postcondition_ axiomatization.

Using the proof assistant Coq, we have formally verified the soundness and
completeness proofs of the axiomatization of the DSL modalities. All our
results can be readily extended to a programming language involving
(sequential) control structures such as loops.

#### Acknowledgments

The authors are grateful for the constructive feedback provided by the
anonymous referees.

##  2 Syntax and semantics

We follow the presentation of SL in [19]. A heap222All italicized variables
are typical meta-variables, and we use primes and subscripts for other meta-
variables of the same type, e.g. $h$, $h^{\prime}$, $h^{\prime\prime}$,
$h_{1}$, $h_{2}$ are all heaps. $h$ is represented by a (finitely-based)
_partial_ function ${\mathbb{Z}\rightharpoonup\mathbb{Z}}$ and the domain of
$h$ is denoted by $\mbox{\it dom}(h)$. We write $h(n)=\bot$ if
$n\not\in\mbox{\it dom}(h)$. The heaps $h,h^{\prime}$ are disjoint iff
$\mbox{\it dom}(h)\cap\mbox{\it dom}(h^{\prime})=\emptyset$. A heap $h$ is
partitioned in $h_{1}$ and $h_{2}$, denoted by $h=h_{1}\uplus h_{2}$, iff
$h_{1}$ and $h_{2}$ are disjoint, $\mbox{\it dom}(h)=\mbox{\it
dom}(h_{1})\cup\mbox{\it dom}(h_{2})$, and $h(n)=h_{i}(n)$ if $n\in\mbox{\it
dom}(h_{i})$ for $i\in\\{1,2\\}$.

$V$ denotes a countably infinite set of integer variables, with typical
element $x$. A store $s$ is a total function $V\rightarrow\mathbb{Z}$. We
abstract from the syntax of arithmetic expressions $e$, and Boolean
expressions $b$. By $\mathit{var}(e)$ (resp. $\mathit{var}(b)$) we denote the
finite set of variables that occur in $e$ (resp. $b$). We have the Boolean
constants true and false, and $(e_{1}=e_{2})$ is a Boolean expression given
arithmetic expressions $e_{1}$ and $e_{2}$. By $s(e)$ we denote the integer
value of $e$ in $s$, and by $s(b)$ we denote the Boolean value of $b$ in $s$.
Following [19] expressions thus do not refer to the heap. By $s[x:=v]$ and
$h[n:=v]$ we denote the result of updating the value of the variable $x$ and
the location $n$, respectively. The definition of $h[n:=v]$ does not require
that $n\in\mbox{\it dom}(h)$. More specifically, we have

$h[n:=v](m)=\left\\{\begin{array}[]{ll}v&\mbox{if $n=m$}\\\
h(m)&\mbox{otherwise}\end{array}\right.$

Thus, $\mbox{\it dom}(h[n:=v])=\mbox{\it dom}(h)\cup\\{n\\}$. For heaps we
also define the clearing of a location, denoted by $h[n:=\bot]$. We have
$h[n:=\bot](m)=\bot$ if $n=m$, and $h[n:=\bot](m)=h(m)$ otherwise. Similarly,
we have $\mathit{dom}(h[n:=\bot])=\mathit{dom}(h)\setminus\\{n\\}$.

Following [19], we have the following basic instructions: $x:=e$ (simple
assignment), $x:=[e]$ (look-up), $[x]:=e$ (mutation), $x:=\mbox{{\bf
cons}}(e)$ (allocation), $\mbox{{\bf dispose}}(x)$ (de-allocation). Just like
[10],

> _We will not give a full syntax of [statements], as the treatment of
> conditionals and looping statements is standard. Instead, we will
> concentrate on assignment statements, which is where the main novelty of the
> approach lies._

The successful execution of any basic instruction $S$ is denoted by $\langle
S,h,s\rangle\Rightarrow(h^{\prime},s^{\prime})$, whereas $\langle
S,h,s\rangle\Rightarrow\mbox{\bf fail}$ denotes a failing execution (e.g. due
to access of a ‘dangling pointer’). See Figure 1 for their semantics (and see
Appendix, Figure 4, for the full syntax and semantics).

$\langle x:=e,h,s\rangle\Rightarrow(h,s[x:=s(e)])$,
$\langle x:=[e],h,s\rangle\Rightarrow(h,s[x:=h(s(e))])$ if $s(e)\in\mbox{\it
dom}(h)$,
$\langle x:=[e],h,s\rangle\Rightarrow\mbox{\bf fail}$ if $s(e)\not\in\mbox{\it
dom}(h)$,
$\langle[x]:=e,h,s\rangle\Rightarrow(h[s(x):=s(e)],s)$ if $s(x)\in\mbox{\it
dom}(h)$,
$\langle[x]:=e,h,s\rangle\Rightarrow\mbox{\bf fail}$ if $s(x)\not\in\mbox{\it
dom}(h)$,
$\langle x:=\mbox{{\bf cons}}(e),h,s\rangle\Rightarrow(h[n:=s(e)],s[x:=n])$
where $n\not\in\mbox{\it dom}(h)$.
$\langle\mbox{{\bf dispose}}(x),h,s\rangle\Rightarrow(h[s(x):=\bot],s)$ if
$s(x)\in\mbox{\it dom}(h)$,
$\langle\mbox{{\bf dispose}}(x),h,s\rangle\Rightarrow\mbox{\bf fail}$ if
$s(x)\not\in\mbox{\it dom}(h)$.

Figure 1: Semantics of basic instructions of heap manipulating programs.

We follow [10] in the definition of the syntax and semantics of the assertion
language of SL but we use a different atomic ‘weak points to’ formula (as in
[18] and [6]). In DSL we have additionally a modality for each statement $S$,
which has highest binding priority.

$p,q\Coloneqq b\mid(e\hookrightarrow e^{\prime})\mid(p\to q)\mid(\forall
xp)\mid(p\mathrel{*}q)\mid(p\mathrel{-\kern-1.99997pt*}q)\mid[S]p$

By $h,s\models p$ we denote the truth relation of classical SL, see Figure 2.
Validity of $p$ is denoted by $\models p$. Semantics of DSL extends the
semantics of SL by giving semantics to the modality, expressing the weakest
precondition. We further have the usual abbreviations: $\lnot p$ denotes
${(p\to\mbox{{\bf false}})}$, $(p\lor q)$ denotes $(\lnot p\to q)$ (negation
has binding priority over implication), $p\equiv q$ denotes $(p\to
q)\wedge(q\to p)$, $(\exists xp)$ denotes $\lnot(\forall x(\lnot p))$ and note
that $x$ is bound in $p$. By logical connective we mean the connectives
$\lnot,\land,\lor,\to,\forall,\exists$, and by separating connective we mean
$\mathrel{*}$ and $\mathrel{-\kern-1.99997pt*}$. Further,
${(e\hookrightarrow-)}$ denotes ${\exists x(e\hookrightarrow x)}$ for a fresh
$x$, emp denotes ${\forall x(x\kern
1.99997pt\not\kern-1.99997pt\hookrightarrow-)}$, and ${(e\mapsto e^{\prime})}$
denotes ${(e\hookrightarrow e^{\prime})}\land(\forall
x({(x\hookrightarrow-)}\to x=e))$ for a fresh $x$. We use
$\not\hookrightarrow$ and $\not=$ as negations of the predicate as usual, and
in particular $(e\kern 1.99997pt\not\kern-1.99997pt\hookrightarrow-)$ is
$\lnot\exists x(e\hookrightarrow x)$. We may drop matching parentheses if
doing so would not give rise to ambiguity. Note that $h,s\models\mbox{\bf
emp}$ iff $\mbox{\it dom}(h)=\emptyset$, and $h,s\models(e\mapsto e^{\prime})$
iff $\mbox{\it dom}(h)=\\{s(e)\\}$ and $h(s(e))=s(e^{\prime})$. An assertion
is _first-order_ if its construction does not involve separating connectives
or modalities.

$h,s\models b$ iff $s(b)=\mbox{{\bf true}}$,
$h,s\models(e\hookrightarrow e^{\prime})$ iff $s(e)\in\mbox{\it dom}(h)$ and
$h(s(e))=s(e^{\prime})$,
$h,s\models(p\land q)$ iff $h,s\models p$ and $h,s\models q$,
$h,s\models(p\to q)$ iff $h,s\models p$ implies $h,s\models q$,
$h,s\models(\forall xp)$ iff $h,s[x:=n]\models p$ for all $n$,
$h,s\models(p\mathrel{*}q)$ iff $h_{1},s\models p$ and $h_{2},s\models q$ for
some $h_{1},h_{2}$ such that $h=h_{1}\uplus h_{2}$,
$h,s\models(p\mathrel{-\kern-1.99997pt*}q)$ iff $h^{\prime},s\models p$
implies $h^{\prime\prime},s\models q$ for all $h^{\prime},h^{\prime\prime}$
such that $h^{\prime\prime}=h\uplus h^{\prime}$,
$h,s\models[S]p$ iff $\langle S,h,s\rangle\not\Rightarrow\mbox{\bf fail}$ and
$h^{\prime},s^{\prime}\models p$ for all $h^{\prime},s^{\prime}$ such that
$\langle S,h,s\rangle\Rightarrow(h^{\prime},s^{\prime})$.

Figure 2: Semantics of Dynamic Separation Logic.

The assertion ${(e\hookrightarrow e^{\prime})}$ is implied by ${(e\mapsto
e^{\prime})}$, and to express the latter using the former requires the use of
separating connectives (i.e. ${(e\hookrightarrow e^{\prime})}$ is equivalent
to ${\mbox{{\bf true}}\mathrel{*}(e\mapsto e^{\prime})}$), whereas our
definition of ${(e\mapsto e^{\prime})}$ requires only logical connectives, and
thus we use ${(e\hookrightarrow e^{\prime})}$ as atomic formula.

A specification $\\{{p}\\}\ {S}\ \\{{q}\\}$ is a triple that consists of a
precondition $p$, a program $S$, and a postcondition $q$. Specifications are
interpreted in the sense of strong partial correctness, which ensures absence
of explicit failure. Formally, following [19], the validity of a
specification, denoted $\models\\{{p}\\}\ {S}\ \\{{q}\\}$, is defined as: if
$h,s\models p$, then $\langle S,h,s\rangle\not\Rightarrow\mbox{\bf fail}$ and
also $\langle S,h,s\rangle\Rightarrow(h^{\prime},s^{\prime})$ implies
$h^{\prime},s^{\prime}\models q$ for all $h^{\prime},s^{\prime}$.

Note that we have that $\models\\{{[S]q}\\}\ {S}\ \\{{q}\\}$ holds, and
$\models\\{{p}\\}\ {S}\ \\{{q}\\}$ implies $\models p\to[S]q$, that is, $[S]q$
is the weakest precondition of statement $S$ and postcondition $q$.

##  3 A sound and complete axiomatization of DSL

In dynamic logic axioms are introduced to simplify formulas in which
modalities occur. For example, we have the following basic equivalences E1-3
for simple assignments.

######  Lemma 3.1 (Basic equivalences).

Let $S$ denote a simple assignment $x:=e$ and $\circ$ denote a (binary)
logical or separating connective.

$\displaystyle[S]\mbox{{\bf false}}$ $\displaystyle\equiv\mbox{{\bf false}}$
(E1) $\displaystyle[S](p\circ q)$ $\displaystyle\equiv[S]p\circ[S]q$ (E2)
$\displaystyle[S](\forall yp)$ $\displaystyle\equiv\forall y([S]p)$ (E3)

In E3 we assume that $y$ does not appear in $S$, neither in the left-hand-side
of the assignment $S$ nor in its right-hand-side.

The proofs of these equivalences proceed by a straightforward induction on the
structure of $p$, where the base cases of Boolean expressions and the weak
points to predicate are handled by a straightforward extension of the
_substitution lemma_ for standard first-order logic. By $b[e/x]$ we denote the
result of replacing every occurrence of $x$ in the Boolean expression $b$ by
the expression $e$ (and similar for arithmetic expressions).

######  Lemma 3.2 (Substitution lemma).

$[x:=e]b\equiv b[e/x]\qquad[x:=e](e^{\prime}\hookrightarrow
e^{\prime\prime})\equiv(e^{\prime}[e/x]\hookrightarrow e^{\prime\prime}[e/x])$
(E4)

######  Proof 3.3.

This lemma follows from the semantics of simple assignment modality and the
substitution lemma of first-order expressions:
$s(e^{\prime}[e/x])=s[x:=s(e)](e^{\prime})$. Note that expressions do not
refer to the heap.

The above equivalences E1-3 do not hold in general for the other basic
instructions. For example, we have ${[x:=[e]]\mbox{{\bf
false}}\equiv\neg(e\hookrightarrow-)}$. On the other hand, ${[x:=\mbox{{\bf
cons}}(0)]\mbox{{\bf false}}\equiv\mbox{{\bf false}}}$, but ${[x:=\mbox{{\bf
cons}}(0)](x\not=0)}$ is not equivalent to $\neg([x:=\mbox{{\bf
cons}}(0)](x=0))$, because $[x:=\mbox{{\bf cons}}(0)](x\not=0)$ is equivalent
to $(0\hookrightarrow-)$ (‘zero is allocated’), whereas $\neg([x:=\mbox{{\bf
cons}}(0)](x=0)$) expresses that $(n\not\hookrightarrow-)$, for some $n\not=0$
(which holds for any finite heap).

The above equivalences E1-3, with E2 restricted to the (standard) logical
connectives, _do_ hold for the _pseudo_ instructions $\langle x\rangle:=e$, a
so-called _heap update_ , and $\langle x\rangle:=\bot$, a so-called _heap
clear_. These pseudo instructions are defined by the transitions

$\langle\langle x\rangle:=e,h,s\rangle\Rightarrow(h[s(x):=s(e)],s)\mbox{ and
}\langle\langle x\rangle:=\bot,h,s\rangle\Rightarrow(h[s(x):=\perp],s)$

In contrast to the mutation and de-allocation instructions, these pseudo-
instructions do not require that $s(x)\in{\it dom}(h)$, e.g., if
$s(x)\not\in{\it dom}(h)$ then the heap update $\langle x\rangle:=e$ extends
the domain of the heap, whereas $[x]:=e$ leads to failure in that case. From a
practical viewpoint, the heap update and heap clear pseudo-instructions are
‘lower level’ instructions, e.g. in processors that implement virtual memory
(where an operating system allocates memory on the fly whenever a program
performs a write to a virtual address that is not allocated), and on top of
these instructions efficient memory allocation algorithms are implemented,
e.g. malloc and free in C. In the following lemma we give an axiomatization in
DSL of the basic SL instructions in terms of simple assignments and these two
pseudo-instructions. For comparison we also give the standard SL
axiomatization [19, 8, 3].

######  Lemma 3.4 (Axioms basic instructions).

$\displaystyle[x:=[e]]p$ $\displaystyle\equiv\exists y((e\hookrightarrow
y)\wedge[x:=y]p),$ (E5) $\displaystyle[[x]:=e]p$
$\displaystyle\equiv\left\\{\begin{array}[]{l}(x\hookrightarrow-)\wedge[\langle
x\rangle:=e]p\\\ (x\mapsto-)\mathrel{*}((x\mapsto
e)\mathrel{-\kern-1.99997pt*}p)\\\ \end{array}\right.$
$\displaystyle[x:=\mbox{{\bf cons}}(e)]p$
$\displaystyle\equiv\left\\{\begin{array}[]{l}\forall
x((x\not\hookrightarrow-)\rightarrow[\langle x\rangle:=e]p)\\\ \forall
x((x\mapsto e)\mathrel{-\kern-1.99997pt*}p)\\\ \end{array}\right.$
$\displaystyle[\mbox{{\bf dispose}}(x)]p$
$\displaystyle\equiv\left\\{\begin{array}[]{l}(x\hookrightarrow-)\wedge[\langle
x\rangle:=\bot]p\\\ (x\mapsto-)\mathrel{*}p\end{array}\right.$

Note that $[x:=y]p$ in E5 reduces to $p[y/x]$ by E1-4. For technical
convenience only, we require in the axioms for ${x:=\mbox{{\bf cons}}(e)}$
that $x$ does not appear in $e$ (see Section 5 to lift this restriction).

In the sequel E5-8 refer to the corresponding DSL equivalences. The proofs of
these equivalences are straightforward (consist simply of expanding the
semantics of the involved modalities) and therefore omitted.

We have the following SL axiomatization of the heap update and heap clear
pseudo-instructions.

$\displaystyle[\langle x\rangle:=e]p$
$\displaystyle\equiv((x\mapsto-)\mathrel{*}((x\mapsto
e)\mathrel{-\kern-1.99997pt*}p))\lor((x\kern
1.99997pt\not\kern-1.99997pt\hookrightarrow-)\land((x\mapsto
e)\mathrel{-\kern-1.99997pt*}p))$ $\displaystyle[\langle x\rangle:=\bot]p$
$\displaystyle\equiv((x\mapsto-)\mathrel{*}p)\lor((x\kern
1.99997pt\not\kern-1.99997pt\hookrightarrow-)\land p)$

This axiomatization thus requires a case distinction between whether or not
$x$ is allocated.

For the complementary approach, we want to resolve the modalities for the heap
update and heap clear instructions compositionally in terms of $p$. What thus
remains for a complete axiomatization is a characterization of $[S]b$,
$[S](e\hookrightarrow e^{\prime})$, $[S](p\mathrel{*}q)$, and
$[S](p\mathrel{-\kern-1.99997pt*}q)$, where $S$ denotes one of the two pseudo-
instructions. Lemma 3.5 provides an axiomatization in DSL of a heap update.

######  Lemma 3.5 (Heap update).

We have the following equivalences for the heap update modality.

$\displaystyle[\langle x\rangle:=e]b$ $\displaystyle\equiv b,$ (E9)
$\displaystyle[\langle x\rangle:=e](e^{\prime}\hookrightarrow
e^{\prime\prime})$ $\displaystyle\equiv(x=e^{\prime}\wedge
e^{\prime\prime}=e)\vee(x\not=e^{\prime}\wedge e^{\prime}\hookrightarrow
e^{\prime\prime}),$ (E10) $\displaystyle[\langle x\rangle:=e](p\mathrel{*}q)$
$\displaystyle\equiv([\langle
x\rangle:=e]p\mathrel{*}q^{\prime})\vee(p^{\prime}\mathrel{*}[\langle
x\rangle:=e]q),$ (E11) $\displaystyle[\langle
x\rangle:=e](p\mathrel{-\kern-1.99997pt*}q)$ $\displaystyle\equiv
p^{\prime}\mathrel{-\kern-1.99997pt*}[\langle x\rangle:=e]q,$ (E12)

where $p^{\prime}$ abbreviates $p\wedge(x\not\hookrightarrow-)$ and,
similarly, $q^{\prime}$ abbreviates $q\wedge(x\not\hookrightarrow-)$.

These equivalences we can informally explain as follows. Since the heap update
$\langle x\rangle:=e$ does not affect the store, and the evaluation of a
Boolean condition $b$ only depends on the store, we have that $([\langle
x\rangle:=e]b)\equiv b$.

Predicting whether ${(e^{\prime}\hookrightarrow e^{\prime\prime})}$ holds
after $\langle x\rangle:=e$, we only need to make a distinction between
whether $x$ and $e^{\prime}$ are aliases, that is, whether they denote the
same location, which is simply expressed by $x=e^{\prime}$. If $x=e^{\prime}$
then $e^{\prime\prime}=e$ should hold, otherwise $(e^{\prime}\hookrightarrow
e^{\prime\prime})$ (note again, that $\langle x\rangle:=e$ does not affect the
values of the expressions $e,e^{\prime}$ and $e^{\prime\prime}$). As a basic
example, we compute

$\begin{array}[]{lll}[\langle
x\rangle:=e](y\hookrightarrow-)&\equiv&(\mbox{definition
}y\hookrightarrow-)\\\ [\langle x\rangle:=e]\exists z(y\hookrightarrow
z)&\equiv&(\mbox{\bf E3})\\\ \exists z[\langle x\rangle:=e](y\hookrightarrow
z)&\equiv&(\mbox{\bf E10})\\\ \exists z((y=x\wedge
e=z)\vee(y\not=x\wedge(y\hookrightarrow z)))&\equiv&(\mbox{semantics SL})\\\
y\not=x\to(y\hookrightarrow-)\end{array}$

We use this derived equivalence in the following example:

$\begin{array}[]{lll}[\langle x\rangle:=e](y\mapsto-)&\equiv&(\mbox{definition
$y\mapsto-$})\\\ [\langle x\rangle:=e]((y\hookrightarrow-)\wedge\forall
z((z\hookrightarrow-)\to z=y))&\equiv&(\mbox{\bf E2, E3, E9})\\\ [\langle
x\rangle:=e](y\hookrightarrow-)\wedge\forall z([\langle
x\rangle:=e](z\hookrightarrow-)\to z=y)&\equiv&(\mbox{see above})\\\
(y\not=x\to(y\hookrightarrow-))\wedge\forall
z((z\not=x\to(z\hookrightarrow-))\to z=y)&\equiv&(\mbox{semantics SL})\\\
y=x\wedge({\bf emp}\vee(x\mapsto-))\end{array}$

Predicting whether $(p\mathrel{*}q)$ holds after the heap update $\langle
x\rangle:=e$, we need to distinguish between whether $p$ or $q$ holds for the
sub-heap that contains the (updated) location $x$. Since we do not assume that
$x$ is already allocated, we instead distinguish between whether $p$ or $q$
holds initially for the sub-heap that does _not_ contain the updated location
$x$. As a simple example, we compute

$\begin{array}[]{lll}[\langle x\rangle:=e](\mbox{{\bf
true}}\mathrel{*}(x\mapsto-))&\equiv&(\mbox{\bf E9,E11})\\\ (\mbox{{\bf
true}}\mathrel{*}((x\mapsto-)\wedge(x\not\hookrightarrow-)))\vee((x\not\hookrightarrow-)\mathrel{*}[\langle
x\rangle:=e](x\mapsto-)&\equiv&(\mbox{see above})\\\ (\mbox{{\bf
true}}\mathrel{*}((x\mapsto-)\wedge(x\not\hookrightarrow-)))\vee((x\not\hookrightarrow-)\mathrel{*}({\bf
emp}\vee(x\mapsto-)))&\equiv&(\mbox{semantics SL})\\\ (\mbox{{\bf
true}}\mathrel{*}\mbox{{\bf
false}})\vee((x\not\hookrightarrow-)\mathrel{*}({\bf
emp}\vee(x\mapsto-)))&\equiv&(\mbox{semantics SL})\\\ \mbox{{\bf
true}}\end{array}$

Note that this coincides with the above calculation of $[\langle
x\rangle:=e](y\hookrightarrow-)$, which also reduces to true, instantiating
$y$ by $x$.

The semantics of $(p\mathrel{-\kern-1.99997pt*}q)$ after the heap update
$\langle x\rangle:=e$ involves universal quantification over all disjoint
heaps that do not contain $x$ (because after the heap update $x$ is
allocated). Therefore we simply add the condition that $x$ is not allocated to
$p$, and apply the heap update to $q$. As a very basic example, we compute

$\begin{array}[]{lll}[\langle x\rangle:=0]((y\hookrightarrow
1)\mathrel{-\kern-1.99997pt*}(y\hookrightarrow 1))&\equiv&(\mbox{\bf E12})\\\
((y\mapsto 1)\wedge(x\not\hookrightarrow-))\mathrel{-\kern-1.99997pt*}[\langle
x\rangle:=0](y\hookrightarrow 1))&\equiv&(\mbox{\bf E10})\\\ ((y\mapsto
1)\wedge(x\not\hookrightarrow-))\mathrel{-\kern-1.99997pt*}((y=x\wedge
0=1)\vee(y\not=x\wedge y\hookrightarrow 1))&\equiv&(\mbox{semantics SL})\\\
\mbox{{\bf true}}\end{array}$

Note that $(y\hookrightarrow 1)\mathrel{-\kern-1.99997pt*}(y\hookrightarrow
1)\equiv\mbox{{\bf true}}$ and $[\langle x\rangle:=0]\mbox{{\bf
true}}\equiv\mbox{{\bf true}}$.

Proof of Lemma 3.5.

E9

$h,s\models[\langle x\rangle:=e]b$
iff (semantics heap update modality)
$h[s(x):=s(e)],s\models b$
iff ($b$ does not depend on the heap)
$h,s\models b$

E10

$h,s\models[\langle x\rangle:=e](e^{\prime}\hookrightarrow e^{\prime\prime})$
iff (semantics heap update modality)
$h[s(x):=s(e)],s\models e^{\prime}\hookrightarrow e^{\prime\prime}$
iff (semantics points-to)
$h[s(x):=s(e)](s(e^{\prime}))=s(e^{\prime\prime})$
iff (definition $h[s(x):=s(e)]$)
if $s(x)=s(e^{\prime})$ then $s(e)=s(e^{\prime\prime})$ else
$h(s(e^{\prime}))=s(e^{\prime\prime})$
iff (semantics assertions)
$h,s\models(x=e^{\prime}\wedge e^{\prime\prime}=e)\vee(x\not=e^{\prime}\wedge
e^{\prime}\hookrightarrow e^{\prime\prime})$

E11

$h,s\models[\langle x\rangle:=e](p*q)$
iff (semantics heap update modality)
$h[s(x):=s(e)],s\models p\mathrel{*}q$.
From here we proceed as follows. By the semantics of separating conjunction,
there exist $h_{1}$ and $h_{2}$ such that $h[s(x):=s(e)]=h_{1}\uplus h_{2}$,
$h_{1},s\models p$, and $h_{2},s\models q$. Let $s(x)\in{\it dom}(h_{1})$ (the
other case runs similarly). So $h[s(x):=s(e)]=h_{1}\uplus h_{2}$ implies
$h_{1}(s(x))=s(e)$ and $h=h_{1}[s(x):=h(x)]\uplus h_{2}$, By the semantics of
the heap update modality, $h_{1}(s(x))=s(e)$ and $h_{1},s\models p$ implies
$h_{1}[s(x):=h(x)],s\models[\langle x\rangle:=e]p$. Since $s(x)\not\in{\it
dom}(h_{2})$, we have $h_{2},s\models q\wedge x\not\hookrightarrow-$. By the
semantics of separation conjunction we conclude that $h,s\models[\langle
x\rangle:=e]p\mathrel{*}q^{\prime}$ ($q^{\prime}$ denotes $q\wedge
x\not\hookrightarrow-$).

In the other direction, from $h,s\models[\langle
x\rangle:=e]p\mathrel{*}q^{\prime}$ (the other case runs similarly) we derive
that there exist $h_{1}$ and $h_{2}$ such that $h=h_{1}\uplus h_{2}$,
$h_{1},s\models[\langle x\rangle:=e]p$ and $h_{2},s\models q^{\prime}$. By the
semantics of the heap update modality it follows that
$h_{1}[s(x):=s(e)],s\models p$. Since $s(x)\not\in{\it dom}(h_{2})$, we have
that $h[s(x):=s(e)]=h_{1}[s(x):=s(e)]\uplus h_{2}$, and so
$h[s(x):=s(e)],s\models p\mathrel{*}q$, that is, $h,s\models[\langle
x\rangle:=e](p\mathrel{*}q)$.

E12

$h,s\models[\langle x\rangle:=e](p\mathrel{-\kern-1.99997pt*}q)$
iff (semantics of heap update modality)
$h[s(x):=s(e)],s\models p\mathrel{-\kern-1.99997pt*}{}q$
iff (semantics separating implication)
for every $h^{\prime}$ disjoint from $h[s(x):=s(e)]$: if $h^{\prime},s\models
p$ then $h[s(x):=s(e)]\uplus h^{\prime},s\models q$
iff (since $s(x)\not\in{\it dom}(h^{\prime})$)
for every $h^{\prime}$ disjoint from $h$: if $h^{\prime},s\models p\wedge
x\not\hookrightarrow-$ then $(h\uplus h^{\prime})[s(x):=s(e)],s\models q$
iff (semantics of heap update modality)
for every $h^{\prime}$ disjoint from $h$: if $h^{\prime},s\models p\wedge
x\not\hookrightarrow-$ then $h\uplus h^{\prime},s\models[s(x):=s(e)]q$
iff (semantics separating implication)
$h,s\models(p\wedge x\not\hookrightarrow-)\mathrel{-\kern-1.99997pt*}[\langle
x\rangle:=e]q$. $\square$

The equivalences for the heap clear modality in the following lemma can be
informally explained as follows: Since $\langle x\rangle:=\bot$ does not
affect the store, and the evaluation of a Boolean condition $b$ only depends
on the store, we have that $[\langle x\rangle:=\bot]b=b$. For
$e\hookrightarrow e^{\prime}$ to hold after executing $\langle
x\rangle:=\bot$, we must initially have that $x\not=e$ and $e\hookrightarrow
e^{\prime}$. As a simple example, we have that $\forall
y,z(y\not\hookrightarrow z)$ characterizes the empty heap. It follows that
$[\langle x\rangle:=\bot](\forall y,z(y\not\hookrightarrow z))$ is equivalent
to $\forall y,z(\neg(y\not=x\wedge y\hookrightarrow z))$. The latter first-
order formula is equivalent to $\forall y,z(y=x\vee y\not\hookrightarrow z)$.
This assertion thus states that the domain consists at most of the location
$x$, which indeed ensures that after $\langle x\rangle:=\bot$ the heap is
empty. To ensure that $p\mathrel{*}q$ holds after clearing $x$ it suffices to
show that the initial heap can be split such that both $p$ and $q$ hold in
their respective sub-heaps with $x$ cleared. The semantics of
$p\mathrel{-\kern-1.99997pt*}q$ after clearing $x$ involves universal
quantification over all disjoint heaps that do may contain $x$, whereas before
executing $\langle x\rangle:=\bot$ it involves universal quantification over
all disjoint heaps that do _not_ contain $x$, in case $x$ is allocated
initially. To formalize in the initial configuration universal quantification
over all disjoint heaps we distinguish between all disjoint heaps that do not
contain $x$ and _simulate_ all disjoint heaps that contain $x$ by interpreting
both $p$ and $q$ in $p\mathrel{-\kern-1.99997pt*}q$ in the context of heap
updates $\langle x\rangle:=y$ with _arbitrary_ values $y$ for the location
$x$. As a very basic example, consider $[\langle
x\rangle:=\bot]((x\hookrightarrow
0)\mathrel{-\kern-1.99997pt*}(x\hookrightarrow 0))$, which should be
equivalent to true. The left conjunct $((x\hookrightarrow
0)\wedge(x\not\hookrightarrow-))\mathrel{-\kern-1.99997pt*}[\langle
x\rangle:=\bot](x\hookrightarrow 0))$ of the resulting formula after applying
E16 is equivalent to true (because $(x\hookrightarrow
0)\wedge(x\not\hookrightarrow-)$ is equivalent to false). We compute the
second conjunct (in the application of E10 we omitted some trivial reasoning
steps):

$\begin{array}[]{lll}\forall y([\langle x\rangle:=y](x\hookrightarrow
0)\mathrel{-\kern-1.99997pt*}[\langle x\rangle:=y](x\hookrightarrow
0)&\equiv&(\mbox{\bf E10})\\\ \forall
y(y=0\mathrel{-\kern-1.99997pt*}y=0)&\equiv&(\mbox{semantics SL})\\\
\mbox{{\bf true}}\end{array}$

######  Lemma 3.6 (Heap clear).

We have the following equivalences for the heap clear modality.

$\displaystyle[\langle x\rangle:=\bot]b$ $\displaystyle\equiv b,$ (E13)
$\displaystyle[\langle x\rangle:=\bot](e\hookrightarrow e^{\prime})$
$\displaystyle\equiv(x\not=e)\wedge(e\hookrightarrow e^{\prime}),$ (E14)
$\displaystyle[\langle x\rangle:=\bot](p*q)$ $\displaystyle\equiv[\langle
x\rangle:=\bot]p\mathrel{*}[\langle x\rangle:=\bot]q,$ (E15)
$\displaystyle[\langle x\rangle:=\bot](p\mathrel{-\kern-1.99997pt*}q)$
$\displaystyle\equiv((p\wedge
x\not\hookrightarrow-)\mathrel{-\kern-1.99997pt*}[\langle
x\rangle:=\bot]q)\wedge\forall y([\langle
x\rangle:=y]p\mathrel{-\kern-1.99997pt*}{}[\langle x\rangle:=y]q),$ (E16)

where $y$ is fresh.

######  Proof 3.7.

Here we go.

E13

$[\langle x\rangle:=\bot]b\equiv b$. As above, it suffices to observe that the
evaluation of $b$ does not depend on the heap.

E14

$h,s\models[\langle x\rangle:=\bot](e\hookrightarrow e^{\prime})$
iff (semantics heap clear modality)
$h[\langle s(x)\rangle:=\bot],s\models e\hookrightarrow e^{\prime}$
iff (semantics points-to)
$s(e)\in{\it dom}(h[\langle s(x)\rangle:=\bot])$ and $h[\langle
s(x)\rangle:=\bot](s(e))=h(s(e))=s(e^{\prime})$
iff (semantics assertions)
$h,s\models x\not=e\wedge e\hookrightarrow e^{\prime}$

E15

$h,s\models[\langle x\rangle:=\bot](p*q)$
iff (semantics heap clear modality)
$h[\langle s(x)\rangle:=\bot],s\models p\mathrel{*}q$
iff (semantics separating conjunction)
$h_{1},s\models p$ and $h_{2},s\models q$, for some $h_{1},h_{2}$ such that
$h[\langle s(x)\rangle:=\bot]=h_{1}\uplus h_{2}$
iff (semantics heap clear modality)
$h_{1},s\models[\langle x\rangle:=\bot]p$ and $h_{2},s\models[\langle
x\rangle:=\bot]q$, for some $h_{1},h_{2}$ such that $h=h_{1}\uplus h_{2}$.
Note: $h=h_{1}\uplus h_{2}$ implies $h[\langle
s(x)\rangle:=\bot]=h_{1}[\langle s(x)\rangle:=\bot]\uplus h_{2}[\langle
s(x)\rangle:=\bot]$, and, conversely, $h[\langle
s(x)\rangle:=\bot]=h_{1}\uplus h_{2}$ implies there exists
$h^{\prime}_{1},h^{\prime}_{2}$ such that $h=h^{\prime}_{1}\uplus
h^{\prime}_{2}$ and $h_{1}=h^{\prime}_{1}[\langle s(x)\rangle:=\bot]$ and
$h_{2}=h^{\prime}_{2}[\langle s(x)\rangle:=\bot]$.

E16

$h,s\models[\langle x\rangle:=\bot](p\mathrel{-\kern-1.99997pt*}{}q)$
iff (semantics heap clear modality)
$h[s(x):=\perp],s\models p\mathrel{-\kern-1.99997pt*}{}q$.
From here we proceed as follows. First we show that $h,s\models((p\wedge
x\not\hookrightarrow-)\mathrel{-\kern-1.99997pt*}{}[\langle x\rangle:=\bot]q)$
and $h,s\models{\forall y([\langle
x\rangle:=y]p\mathrel{-\kern-1.99997pt*}{}[\langle x\rangle:=y]q)}$ implies
$h[s(x):=\perp],s\models p\mathrel{-\kern-1.99997pt*}{}q$. Let $h^{\prime}$ be
disjoint from $h[s(x):=\perp]$ and $h^{\prime},s\models p$. We have to show
that $h[s(x):=\perp]\uplus h^{\prime},s\models q$. We distinguish the
following two cases.

  * •

First, let $s(x)\in{\it dom}(h^{\prime})$. We then introduce
${s^{\prime}=s[y:=h^{\prime}(s(x))]}$. We have $h^{\prime},s^{\prime}\models
p$ (since $y$ does not occur in $p$), so it follows by the semantics of the
heap update modality that $h^{\prime}[s(x):=\bot],s^{\prime}\models[\langle
x\rangle:=y]p$. Since $h^{\prime}[s(x):=\bot]$ and $h$ are disjoint (which
clearly follows from that $h^{\prime}$ and $h[s(x):=\bot]$ are disjoint), and
since $h,s^{\prime}\models[\langle
x\rangle:=y]p\mathrel{-\kern-1.99997pt*}{}[\langle x\rangle:=y]q$, we have
that $h\uplus(h^{\prime}[s(x):=\bot]),s^{\prime}\models[\langle
x\rangle:=y]q$. Applying again the semantics of the heap update modality, we
obtain
$(h\uplus(h^{\prime}[s(x):=\bot]))[s(x):=s^{\prime}(y)],s^{\prime}\models q$.
We then can conclude this case observing that $y$ does not occur in $q$ and
that $h[s(x):=\bot]\uplus
h^{\prime}=(h\uplus(h^{\prime}[s(x):=\bot]))[s(x):=s^{\prime}(y)]$.

  * •

Next, let $s(x)\not\in{\it dom}(h^{\prime})$. So $h^{\prime}$ and $h$ are
disjoint, and thus (since $h,s\models(p\wedge
x\not\hookrightarrow-)\mathrel{-\kern-1.99997pt*}{}[\langle x\rangle:=\bot]q$)
we have $h\uplus h^{\prime},s\models[\langle x\rangle:=\bot]q$. From which we
derive $(h\uplus h^{\prime})[s(x):=\bot],s\models q$ by the induction
hypothesis. We then can conclude this case by the observation that
${h[s(x):=\bot]\uplus h^{\prime}}={(h\uplus h^{\prime})[s(x):=\bot]}$.

Conversely, assuming $h[s(x):=\bot],s\models p\mathrel{-\kern-1.99997pt*}{}q,$
we first show that $h,s\models(p\wedge
x\not\hookrightarrow-)\mathrel{-\kern-1.99997pt*}{}[\langle x\rangle:=\bot]q$
and then $h,s\models\forall y([\langle
x\rangle:=y]p\mathrel{-\kern-1.99997pt*}{}[\langle x\rangle:=y]q).$

  * •

Let $h^{\prime}$ be disjoint from $h$ and $h^{\prime},s\models p\wedge
x\not\hookrightarrow-$. We have to show that $h\uplus
h^{\prime},s\models[\langle x\rangle:=\bot]q$, that is, $(h\uplus
h^{\prime})[s(x):=\perp],s\models q$ (by the semantics of the heap clear
update). Clearly, $h[s(x):=\bot]$ and $h^{\prime}$ are disjoint, and so
$h[s(x):=\bot]\uplus h^{\prime},s\models q$ follows from our assumption. We
then can conclude this case by the observation that $(h\uplus
h^{\prime})[s(x):=\bot]=h[s(x):=\bot]\uplus h^{\prime}$, because
$s(x)\not\in{\it dom}(h^{\prime})$.

  * •

Let $h^{\prime}$ be disjoint from $h$ and $s^{\prime}=s[y:=n]$, for some $n$
such that $h^{\prime},s^{\prime}\models[\langle x\rangle:=y]p$. We have to
show that $h\uplus h^{\prime},s^{\prime}\models[\langle x\rangle:=y]q$. By the
semantics of the heap update modality it follows that
$h^{\prime}[s(x):=n],s^{\prime}\models p$, that is,
$h^{\prime}[s(x):=n],s\models p$ (since $y$ does not occur in $p$). Since
$h^{\prime}[s(x):=n]$ and $h[s(x):=\bot]$ are disjoint, we derive from the
assumption $h[s(x):=\bot],s\models p\mathrel{-\kern-1.99997pt*}{}q$ that
$h[s(x):=\bot]\uplus h^{\prime}[s(x):=n],s\models q$. Again by the semantics
of the heap update modality we have that $h\uplus
h^{\prime},s^{\prime}\models[\langle x\rangle:=y]q$ iff $(h\uplus
h^{\prime})[s(x):=n],s^{\prime}\models q$ (that is, $(h\uplus
h^{\prime})[s(x):=n],s\models q$, because $y$ does not occur in $q$). We then
can conclude this case by the observation that ${(h\uplus
h^{\prime})[s(x):=n]}={h[s(x):=\bot]\uplus h^{\prime}[s(x):=n]}$.

We denote by E the _rewrite system_ obtained from the equivalences E1-16 by
orienting these equivalences from left to right, e.g., equivalence E1 is
turned into a rewrite rule $[S]\mbox{{\bf false}}\Rightarrow\mbox{{\bf
false}}$. The following theorem states that the rewrite system E is complete,
that is, confluent and strongly normalizing. Its proof is straightforward
(using standard techniques) and therefore omitted.

######  Theorem 3.8 (Completeness of E).

  * •

Normal form. Every standard formula $p$ of SL is in normal form (which means
that it cannot be reduced by the rewrite system E).

  * •

Local confluence. For any two reductions $p\Rightarrow q_{1}$ and
$p\Rightarrow q_{2}$ ($p$ a formula of DSL) there exists a DSL formula $q$
such that $q_{1}\Rightarrow q$ and $q_{2}\Rightarrow q$.

  * •

Termination. There does not exist an infinite chain of reductions
$p_{1}\Rightarrow p_{2}\Rightarrow p_{3}\cdots$.

We now show an example of the interplay between the modalities for heap update
and heap clear. We want to derive

$\\{{\forall x((x\not\hookrightarrow-)\to p)}\\}\ {x:=\mbox{{\bf
cons}}(0);\mbox{{\bf dispose}}(x)}\ \\{{p}\\}$

where statement $x:=\mbox{{\bf cons}}(0);\mbox{{\bf dispose}}(x)$ simulates
the so-called random assignment [9]: the program terminates with a value of
$x$ that is chosen non-deterministically. First we apply the axiom E8 for de-
allocation to obtain

$\\{{(x\hookrightarrow-)\land[\langle x\rangle:=\bot]p}\\}\ {\mbox{{\bf
dispose}}(x)}\ \\{{p}\\}.$

Next, we apply the axiom E8 for allocation to obtain

$\begin{array}[]{c}\\{\forall x((x\kern
1.99997pt\not\kern-1.99997pt\hookrightarrow-)\to[\langle
x\rangle:=0]((x\hookrightarrow-)\land[\langle x\rangle:=\bot]p))\\}\\\
{x:=\mbox{{\bf cons}}(0)}\\\ \\{(x\hookrightarrow-)\land p[\langle
x\rangle:=\bot]\\}.\end{array}$

Applying E10 (after pushing the heap update modality inside), followed by some
basic first-order reasoning, we can reduce $[\langle x\rangle:=0](\exists
y(x\hookrightarrow y))$ to true. So we obtain

$\begin{array}[]{c}\\{\forall x((x\kern
1.99997pt\not\kern-1.99997pt\hookrightarrow-)\to[\langle x\rangle:=0][\langle
x\rangle:=\bot]p)\\}\\\ {x:=\mbox{{\bf cons}}(0)}\\\
\\{(x\hookrightarrow-)\land p[\langle x\rangle:=\bot]\\}.\end{array}$

In order to proceed we formalize the interplay between the modalities for heap
update and heap clear by the following general equivalence:

$[\langle x\rangle:=e][\langle x\rangle:=\bot]p\equiv[\langle
x\rangle:=\bot]p$

We then complete the proof by applying the sequential composition rule and
consequence rule, using the above equivalence and the following axiomatization
of the heap clear modality:

$(x\not\hookrightarrow-)\wedge[\langle
x\rangle:=\bot]p\equiv(x\not\hookrightarrow-)\wedge p$

The above axiomatization can be extended in the standard manner to a program
logic for sequential while programs, see [9], which does not require the frame
rule, nor any other adaptation rule besides the consequence rule. For
recursive programs however one does need more adaptation rules: a further
discussion about the use of the frame rule in a completeness proof for
recursive programs is outside the scope of this paper.

##  4 Expressiveness DSL

In this section, we illustrate the expressiveness of DSL in a completeness
proof of the local mutation axiom and a novel strongest postcondition
axiomatization.

###  4.1 Completeness local axioms

We consider the completeness of the following local mutation axiom
(completeness of the local axioms for the other standard basic instructions
have already been established, as observed in the Introduction)

$\\{{x\mapsto-}\\}\ {[x]:=e}\ \\{{x\mapsto e}\\}$

The proof itself does not make use of the separating implication.

######  Theorem 4.1 (Completeness local mutation axiom).

If $\models\\{{p}\\}\ {[x]:=e}\ \\{{q}\\}$ then $\\{{p}\\}\ {[x]:=e}\
\\{{q}\\}$ is derivable using the local mutation axiom, frame rule, and
consequence rule.

######  Proof 4.2.

The problem here is how to compute a ‘frame’ $r$ for a given valid
specification $\\{{p}\\}\ {[x]:=e}\ \\{{q}\\}$ so that $p$ implies
${(x\mapsto-)\mathrel{*}r}$ and $(x\mapsto e)\mathrel{*}r$ implies $q$. We
show here how the heap update modality can be used to describe such a frame.
Let $\models\\{{p}\\}\ {[x]:=e}\ \\{{q}\\}$ and $r$ denote $\exists y([\langle
x\rangle:=y]p)$ for some fresh $y$. By the local axiom and the frame rule, we
first derive

$\\{{(x\mapsto-)\mathrel{*}r}\\}\ {[x]:=e}\ \\{{(x\mapsto e)\mathrel{*}r}\\}.$

Let $h,s\models p$. To prove that $h,s\models{(x\mapsto-)\mathrel{*}r}$, it
suffices to show that there exists a split ${h=h_{1}\uplus h_{2}}$ such that
$h_{1},s\models{(x\mapsto-)}$ and $h_{2},s[y:=n]\models[\langle
x\rangle:=y]p$, for some $n$. Since $\models\\{{p}\\}\ {[x]:=e}\ \\{{q}\\}$ we
have that $s(x)\in{\it dom}(h)$. So we can introduce the split ${h=h_{1}\uplus
h_{2}}$ such that $h_{1},s\models{(x\mapsto-)}$ and ${h_{2}=h[s(x):=\bot]}$.
By the semantics of the heap update modality it then suffices to observe that
$h_{2},s[y:=h(s(x))]\models[\langle x\rangle:=y]p$ if and only if
$h_{2}[s(x):=h(s(x))],s\models p$ ($y$ does not appear in $p$), that is,
$h,s\models p$.

On the other hand, we have that $(x\mapsto e)\mathrel{*}r$ implies $q$: Let
$h,s\models(x\mapsto e)\mathrel{*}r$. So there exists a split $h=h_{1}\uplus
h_{2}$ such that $h_{1},s\models x\mapsto e$ and $h_{2},s\models r$. Let $n$
be such that $h_{2},s[y:=n]\models[\langle x\rangle:=y]p$. By the semantics of
the heap update modality again we have that ${h_{2},s[y:=n]}\models[\langle
x\rangle:=y]p$ if and only if $h_{2}[s(x):=n],s\models p$ (here $y$ does not
appear in $p$). Since $\models\\{{p}\\}\ {[x]:=e}\ \\{{q}\\}$ it then follows
that ${h_{2}[s(x):=s(e)],s}\models q$, that is, $h,s\models q$ (note that
$h=h_{2}[s(x):=s(e)]$ because $h(s(x))=s(e)$ and $h_{2}=h[s(x):=\bot]$).

###  4.2 Strongest postcondition axiomatization

Before we discuss a novel strongest postcondition axiomatization using the
modalities of DSL, it should be noted that in general the semantics of program
logics which require absence of certain failures gives rise to an asymmetry
between weakest preconditions and strongest postconditions: For any statement
$S$ and postcondition $q$ we have that $\models\\{{\mbox{{\bf false}}}\\}\
{S}\ \\{{q}\\}$. However, for any precondition $p$ which does not exclude
failures, there does not exist _any_ postcondition $q$ such that
$\models\\{{p}\\}\ {S}\ \\{{q}\\}$. We solve this by simply requiring that the
given precondition does not give rise to failures (see below).

${\\{{p}\\}\ {x:=e}\ \\{{\exists y([x:=y]p\wedge(x=e[y/x]))}\\}}{}$
$\\!\\!\\!\\!{\\{{p\wedge(e\hookrightarrow-)}\\}\ {x:=[e]}\ \\{{\exists
y([x:=y]p\wedge(x\hookrightarrow e[y/x]))}\\}}{}$
${\\{{p\wedge(x\hookrightarrow-)}\\}\ {[x]:=e}\ \\{{\exists y([\langle
x\rangle:=y]p)\wedge(x\hookrightarrow e)}\\}}{}$ $\\!\\!{\\{{p}\\}\
{x:=\mbox{{\bf cons}}(e)}\ \\{{[\langle x\rangle:=\bot](\exists
xp)\wedge(x\hookrightarrow e)}\\}}{}$
$\\!\\!{\\{{p\wedge(x\hookrightarrow-)}\\}\ {\mbox{{\bf dispose}}(x)}\
\\{{\exists y([\langle x\rangle:=y]p)\wedge(x\not\hookrightarrow-)}\\}}{}$

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:=\mbox{{\bf cons}}(e)$.

Figure 3 contains our novel strongest postcondition axiomatization SP-DSL,
where the main novelty is in the use of the heap update and heap clear
modalities in the axiomatization of the mutation, allocation, and de-
allocation instruction. It is worthwhile to contrast, for example, the use of
the heap clear modality to express freshness in the strongest postcondition
axiomatization of the allocation instruction with the following traditional
axiom (assuming that $x$ does not occur free in $p$):

$\\{{p}\\}\ {x:=\mbox{{\bf cons}}(e)}\ \\{{p\mathrel{*}(x\mapsto e)}\\}$

where freshness is enforced by the introduction of the separating conjunction
(which as such increases the complexity of the postcondition). More
specifically, we have the following instance of the allocation axiom in Figure
3 (also making use of that $x$ does not appear in the precondition)

$\\{{y\hookrightarrow 0}\\}\ {x:=\mbox{{\bf cons}}(1)}\ \\{{[\langle
x\rangle:=\bot](y\hookrightarrow 0)\wedge(x\hookrightarrow 1)}\\}$

Applying E14 we obtain

$\\{{y\hookrightarrow 0}\\}\ {x:=\mbox{{\bf cons}}(1)}\
\\{{y\not=x\wedge(y\hookrightarrow 0)\wedge(x\hookrightarrow 1)}\\}$

On the other hand, instantiating the above traditional axiom we obtain

$\\{{y\hookrightarrow 0}\\}\ {x:=\mbox{{\bf cons}}(1)}\ \\{{(y\hookrightarrow
0)\mathrel{*}(x\mapsto 1)}\\}$

which is implicit and needs unraveling the semantics of separating
conjunction. Using the heap clear modality we thus obtain a basic assertion in
predicate logic which provides an explicit but simple account of aliasing.

######  Theorem 4.3 (Soundness and completeness SP-DSL).

For any basic instruction $S$, we have $\models\\{{p}\\}\ {S}\ \\{{q}\\}$ if
and only if $\\{{p}\\}\ {S}\ \\{{q}\\}$ is derivable from the axioms in SP-DSL
(Figure 3) and (a single application of) the rule of consequence.

######  Proof 4.4.

We showcase the soundness and completeness of the strongest postcondition
axiomatization of allocation (soundness and completeness of the strongest
postconditions for the mutation and de-allocation instructions follow in a
straightforward manner from the semantics of the heap update modality).

  * •

$\models\\{{p}\\}\ {x:=\mbox{{\bf cons}}(e)}\ \\{{[\langle
x\rangle:=\bot](\exists y([x:=y]p))\wedge x\hookrightarrow e}\\}$:
Let $h,s\models p$. We have to show that ${h[n:=s(e)],s[x:=n]}\models{[\langle
x\rangle:=\bot](\exists y([x:=y]p))}\wedge{x\hookrightarrow e}$, for
$n\not\in{\it dom}(h)$. By definition $h[n:=s(e)],s[x:=n]\models
x\hookrightarrow e$. By the semantics of the heap clear modality and
existential quantification, it then suffices to show that
$h[n:=\perp],s[x:=n][y:=s(x)]\models[x:=y]p$, which by the semantics of the
simple assignment modality boils down to $h,s[y:=s(x)]\models p$ (note that
$n\not\in{\it dom}(h)$, that is, $h,s\models p$ ($y$ does not appear in $p$),
which holds by assumption.

  * •

$\models\\{{p}\\}\ {x:=\mbox{{\bf cons}}(e)}\ \\{{q}\\}$ implies
$\models([\langle x\rangle:=\bot](\exists y(p[x:=y]))\wedge x\hookrightarrow
e)\to q$:
Let $h,s\models[\langle x\rangle:=\bot](\exists y([x:=y]p))\wedge
x\hookrightarrow e$. We have to show that $h,s\models q$. By the semantics of
the heap clear modality we derive from the above assumption that
$h[s(x):=\bot],s\models\exists y(p[x:=y])$. Let
${h[s(x):=\bot],s[y:=n]}\models p[x:=y]$, for some $n$. It follows from the
semantics of the simple assignment modality that
${h[s(x):=\bot],s[x:=n]}\models p$ ($y$ does not appear in $p$). Since
$s(x)\not\in{\it dom}(h[s(x):=\bot])$, we have that ${\langle x:=\mbox{{\bf
cons}}(e),h[s(x):=\bot],s[x:=n]\rangle}\Rightarrow{(h[s(x):=s[x:=n](e)],s)}$.
Since we can assume without loss of generality that $x$ does not occur in $e$
we have that $s[x:=n](e)=s(e)$, and so from the assumption that $h,s\models
x\hookrightarrow e$ we derive that $h[s(x):=s[x:=n](e)]=h$. From $\\{{p}\\}\
{x:=\mbox{{\bf cons}}(e)}\ \\{{q}\\}$ then we conclude that $h,s\models q$.

##  5 Extensions

A straightforward extension concerns the general mutation instruction
$[e]:=e^{\prime}$, which allows the use of an arbitrary arithmetic expression
$e$ to denote the updated location. We can simulate this by the statement
$x:=e;\ [x]:=e^{\prime}$, where $x$ is a fresh variable. Applying the
modalities we derive the following axiom

${\\{{(e\hookrightarrow-)\wedge[x:=e][\langle x\rangle:=e^{\prime}]p}\\}\
{[e]:=e^{\prime}}\ \\{{p}\\}}{}$

where $x$ is a fresh variable.

Another straightforward extension concerns the allocation $x:=\mbox{{\bf
cons}}(e)$ in the case where $x$ does occur in $e$. The instruction
${x:=\mbox{{\bf cons}}(e)}$ can be simulated by ${y:=x;}\ {y:=\mbox{{\bf
cons}}(e[y/x])}$ where $y$ is a fresh variable. Applying the sequential
composition rule and the axiom for basic assignments, it is straightforward to
derive the following generalized backwards allocation axiom:

${\\{{\forall y((y\not\hookrightarrow-)\rightarrow[y:=x][\langle
y\rangle:=e[y/x]]p)}\\}\ {x:=\mbox{{\bf cons}}(e)}\ \\{{p}\\}}{}$

where $y$ is fresh.

Reynolds introduced in [19] the allocation instruction ${x:=\mbox{{\bf
cons}}(\bar{e})}$, which allocates a consecutive part of the memory for
storing the values of $\bar{e}$: its semantics is described by

$\langle x:={\bf
cons}(\bar{e}),h,s\rangle\Rightarrow(h[\bar{m}:=s(\bar{e})],s[x:=m_{1}])$

where $\bar{e}=e_{1},\ldots,e_{n}$, $\bar{m}=m_{1},\ldots,m_{n}$,
$m_{i+1}=m_{i}+1$, for $i=1,\ldots,n-1$,
$\\{m_{1},\ldots,m_{n}\\}\cap\mbox{\it dom}(h)=\emptyset$, and, finally,

$h[\bar{m}:=s(\bar{e})](k)=\left\\{\begin{array}[]{ll}h(k)&\text{if
}k\not\in\\{m_{1},\ldots,m_{n}\\}\\\ s(e_{i})&\text{if }k=m_{i}\text{ for some
}i=1,\ldots,n.\end{array}\right.$

Let $\bar{e}^{\prime}$ denote a sequence of expressions $e^{\prime}_{1},\ldots
e^{\prime}_{n}$ such that $e^{\prime}_{1}$ denotes the variable $x$ and
$e^{\prime}_{i}$ denotes the expression $x+(i-1)$, for $i=2,\ldots,n$. The
storage of the values of $e_{1},\ldots,e_{n}$ then can be modeled by a
sequence of heap update modalities $[\langle e^{\prime}_{i}\rangle:=e_{i}]$,
for $i=1,\ldots,n$. We abbreviate such a sequence by
$[\langle\bar{e}^{\prime}\rangle:=\bar{e}]$. Assuming that $x$ does not occur
in one of the expressions $\bar{e}$ (this restriction can be lifted as
described above), we have the following generalization of the above backwards
allocation axiom

${\\{{\forall
x(\Big{(}\bigwedge_{i=1}^{n}(e^{\prime}_{i}\not\hookrightarrow-)\Big{)}\rightarrow[\langle\bar{e}^{\prime}\rangle:=\bar{e}]p)}\\}\
{x:={\bf cons}(\bar{e})}\ \\{{p}\\}}{}$

#### Recursive predicates

Next we illustrate the extension of our approach to recursive predicates for
reasoning about a linked list. Assuming a set of user-defined predicates
$r(x_{1},\ldots,x_{n})$ of arity $n$, we introduce corresponding basic
assertions $r(e_{1},\ldots,e_{n})$ which are interpreted by (the least fixed
point of) a system of recursive predicate definitions
$r(x_{1},\ldots,x_{n}):=p$, where the user-defined predicates only occur
positively in $p$.

If for any recursive definition $r(x_{1},\ldots,x_{n}):=p$ only the formal
parameters $x_{1},\ldots,x_{n}$ occur free in $p$, we can simply define
$[x:=e]r(e_{1},\ldots,e_{n})$ by ${r(e_{1}[e/x],\ldots,e_{n}[e/x])}$. However,
allowing global variables in recursive predicate definitions does affect the
interpretation of these definitions. As a very simple example, given
$r(y):=x=1$, clearly $\\{{r(y)}\\}\ {x:=0}\ \\{{r(y)}\\}$ is invalid (and so
we cannot simply define $[x:=0]r(y)$ by $r(y[0/x])$). Furthermore,
substituting the parameters of $r$ clearly does not make sense for modalities
with heap modifications (such as mutation, allocation, etc.): as subformulas
may depend on the heap, these may require alias analysis _in the definition of
$r$_.

We illustrate how our dynamic logic works with recursively defined predicates
on a characteristic linked list example. In particular, let $r$ be the
recursively defined _reachability_ predicate

$r(x,y):=x=y\lor\exists z((x\mapsto z)\mathrel{*}r(z,y)).$

We shall prove $\\{{r(\mathit{first},y)}\\}\ {\mathit{first}:=\mbox{{\bf
cons}}(\mathit{first})}\ \\{{r(\mathit{first},y)}\\}$. To do so, we model
$\mathit{first}:=\mbox{{\bf cons}}(\mathit{first})$ by $u:=\mathit{first};\
\mathit{first}:=\mbox{{\bf cons}}(u)$, for some fresh variable $u$. Thus it is
sufficient to show

$\\{{r(\mathit{first},y)}\\}\ {u:=\mathit{first};\ \mathit{first}:=\mbox{{\bf
cons}}(u)}\ \\{{r(\mathit{first},y)}\\}.$

We first calculate the weakest precondition of the last assignment:
$[\mathit{first}:=\mbox{{\bf cons}}(u)]r(\mathit{first},y)$. Using equivalence
(E7) of Lemma 3.4 we obtain $\forall\mathit{first}((\mathit{first}\kern
1.99997pt\not\kern-1.99997pt\hookrightarrow-)\to[\langle\mathit{first}\rangle:=u]r(\mathit{first},y)$.

Next, we simplify the modal subformula
$[\langle\mathit{first}\rangle:=u]r(\mathit{first},y)$ we first unfold the
definition of $r$, obtaining $\mathit{first}=y\lor\exists
z((\mathit{first}\mapsto z)\mathrel{*}r(z,y))$. By Lemma 3.5 (E11),
$[\langle\mathit{first}\rangle:=u](\mathit{first}\mapsto z\mathrel{*}r(z,y))$
reduces to the disjunction of ${(\mathit{first}\mapsto
z\wedge\mathit{first}\kern
1.99997pt\not\kern-1.99997pt\hookrightarrow-)\mathrel{*}[\langle\mathit{first}\rangle:=u]r(z,y))}$
and ${[\langle\mathit{first}\rangle:=u](\mathit{first}\mapsto
z)\mathrel{*}(r(z,y)\wedge\mathit{first}\kern
1.99997pt\not\kern-1.99997pt\hookrightarrow-)}$. In the first disjunct, the
left-hand side of the separating conjunction asserts that $\mathit{first}$ is
allocated (and points to $z$) and that simultaneously $\mathit{first}$ is not
allocated. This clearly is false in every heap, so that whole disjunct reduces
to false. Simplifying the second disjunct (reducing the modality with
equivalence (E10) of Lemma 3.5) and applying standard logical equivalences,
yields that the whole subformula is equivalent to

$\mathit{first}=y\lor(r(u,y)\wedge(\mathit{first}\kern
1.99997pt\not\kern-1.99997pt\hookrightarrow-)).$

Applying the allocation axiom and an application of the consequence rule, we
obtain

$\begin{array}[]{c}\\{\forall\mathit{first}((\mathit{first}\kern
1.99997pt\not\kern-1.99997pt\hookrightarrow-)\to(\mathit{first}=y\lor
r(u,y)))\\}\\\ {\mathit{first}:=\mbox{{\bf cons}}(u)}\\\
\\{r(\mathit{first},y)\\}.\end{array}$

Renaming $\mathit{first}$ by the fresh variable $f$ does not affect $r$, so

$\begin{array}[]{c}\\{\forall f((f\kern
1.99997pt\not\kern-1.99997pt\hookrightarrow-)\to(f=y\lor r(u,y)))\\}\\\
{\mathit{first}:=\mbox{{\bf cons}}(u)}\\\
\\{r(\mathit{first},y)\\}\end{array}$

can be derived. Also substituting $u$ for $\mathit{first}$ does not affect the
definition of $r$. It then suffices to observe that $r(\mathit{first},y)$
(trivially) implies $\forall f((f\kern
1.99997pt\not\kern-1.99997pt\hookrightarrow-)\to(f=y\lor
r(\mathit{first},y)))$.

##  6 Formalization in Coq

The main motivation behind formalizing results in a proof assistant is to
rigorously check hand-written proofs. For our formalization we used the
dependently-typed calculus of inductive constructions as implemented by the
Coq proof assistant. We have used no axioms other than the axiom of function
extensionality (for every two functions $f,g$ we have that $f=g$ if
$f(x)=g(x)$ for all $x$). This means that we work with an underlying
intuitionistic logic: we have not used the axiom of excluded middle for
reasoning classically about propositions. However, the decidable propositions
(propositions $P$ for which the excluded middle $P\lor\lnot P$ can be proven)
allow for a limited form of classical reasoning.

We formalize the basic instructions of our programming language (assignment,
look-up, mutation, allocation, and deallocation) and the semantics of basic
instructions. For Boolean and arithmetic expressions we use a shallow
embedding, so that those expressions can be directly given as a Coq term of
the appropriate type (with a coincidence condition assumed, i.e. that values
of expressions depend only on finitely many variables of the store).

There are two approaches in formalizing the semantics of assertions: shallow
and deep embedding. We have taken both approaches. In the first approach, the
shallow embedding of assertions, we define assertions of DSL by their
extension of satisfiability (i.e. the set of heap and store pairs in which the
assertion is satisfied), that must satisfy a coincidence condition (assertions
depend only on finitely many variables of the store) and a stability condition
(see below). The definition of the modality operator follows from the
semantics of programs, which includes basic control structures such as the
while-loop. In the second approach, the deep embedding of assertions,
assertions are modeled using an inductive type and we explicitly introduce two
meta-operations on assertions that capture the heap update and heap clear
modality. We have omitted the clauses for emp and $(e\mapsto e^{\prime})$,
since these could be defined as abbreviations, and we restrict to the basic
instructions.

In the deep embedding we have no constructor corresponding to the program
modality $[S]p$. Instead, two meta-operations denoted $p[\langle x\rangle=e]$
and $p[\langle x\rangle:=\bot]$ are defined recursively on the structure of
$p$. Crucially, we formalized and proven the following lemmas (the details are
almost the same as showing the equivalences hold in the shallow embedding,
Lemmas 3.5 and 3.6):

######  Lemma 6.1 (Heap update substitution lemma).

${h,s\models p[\langle x\rangle:=e]\text{ iff }h[s(x):=s(e)],s\models p}$.

######  Lemma 6.2 (Heap clear substitution lemma).

${h,s\models p[\langle x\rangle:=\bot]\text{ iff }h[s(x):=\bot],s\models p}$.

By also formalizing a deep embedding, we show that the modality operator can
be defined entirely on the meta-level by introducing meta-operations on
formulas that are recursively defined by the structure of assertions: this
captures Theorem 3.8. The shallow embedding, on the other hand, is easier to
show that our approach can be readily extended to complex programs including
while-loops.

In both approaches, the semantics of assertions is classical, although we work
in an intuitionistic meta-logic. We do this by employing a double negation
translation, following the set-up by R. O’Connor [14]. In particular, we have
that our satisfaction relation $h,s\models p$ is stable, i.e.
$\lnot\lnot(h,s\models p)$ implies $h,s\models p$. This allows us to do
classical reasoning on the image of the higher-order semantics of our
assertions.

The source code of our formalization is accompanied with this paper as a
digital artifact (which includes the files shallow/Language.v and
shallow/Proof.v, and the files deep/Heap.v, deep/Language.v,
deep/Classical.v). The artifact consists of the following files:

  * •

shallow/Language.v: Provides a shallow embedding of Boolean expressions and
arithmetic expressions, and a shallow embedding of our assertion language, as
presented in the prequel.

  * •

shallow/Proof.v: Provides proof of the equivalences (E1-16), and additionally
standard equivalences for modalities involving complex programs.

  * •

deep/Heap.v: Provides an axiomatization of heaps as partial functions.

  * •

deep/Language.v: Provides a shallow embedding of Boolean expressions and
arithmetic expressions, and a deep embedding of our assertion language, on
which we inductively define the meta operations of heap update and heap clear.
We finally formalize Hoare triples and proof systems using weakest
precondition and strongest postcondition axioms for the basic instructions.

  * •

deep/Classical.v: Provides the classical semantics of assertions, and the
strong partial correctness semantics of Hoare triples. Further it provides
proofs of substitution lemmas corresponding to our meta-operators. Finally, it
provides proofs of the soundness and completeness of the aforementioned proof
systems.

##  7 Conclusion and related work

To the best of our knowledge no other works exist that study dynamic logic
extensions of SL. We have shown how we can combine the standard programming
logics in SL with a new DSL axiomatization of both weakest preconditions and
strongest postconditions. These new axiomatizations in DSL have the so-called
property of _gracefulness_ :333The term ‘graceful’, coined by J.C. Blanchette
[22], comes from higher-order automated theorem proving where it means that a
higher-order prover does not perform significantly worse on first-order
problems than existing first-order provers that lack the ability to reason
about higher-order problems. any first-order postcondition gives rise to a
first-order weakest precondition (for any basic instruction). A property that
existing axiomatizations of SL, such as given by C. Bannister, P. Höfner and
G. Klein [3], and M. Faisal Al Ameen and M. Tatsuta [8], lack. (See also
[21].) As a simple example, in our approach $[[x]:=0](y\hookrightarrow z)$ can
be resolved to the first-order formula

$(x\hookrightarrow-)\wedge((y=x\wedge z=0)\vee(y\not=x\wedge y\hookrightarrow
z))$

by applying the above equivalences E6 and E10. The standard rule for backwards
reasoning in [19] however gives the weakest precondition:

$(x\mapsto-)\mathrel{*}((x\mapsto
0)\mathrel{-\kern-1.99997pt*}(y\hookrightarrow z))$

Despite their different formulations, both formulas characterize
$[[x]:=0](y\hookrightarrow z)$, and thus must be equivalent. In fact, the
equivalence has been proven in our Coq formalization (Section 6).
Surprisingly, this however exceeds the capability of all the automated SL
provers in the benchmark competition for SL [20]. In particular, only the
CVC4-SL tool [17] supports the fragment of SL that includes the separating
implication connective. However, from our own experiments with that tool, we
found that it produces an incorrect counter-example and reported this as a bug
to one of the maintainers of the project [16]. In fact, the latest version,
CVC5-SL, reports the same input as ‘unknown’, indicating that the tool is
incomplete. Furthermore, we have investigated whether the equivalence of these
formulas can be proven in an interactive tool for reasoning about SL: the Iris
project [11]. However, also in that system it is not possible to show the
equivalence of these assertions, at least not without adding additional axioms
to its underlying model [12]. On the other hand, the equivalence between the
above two formulas can be expressed in quantifier-free separation logic, for
which a complete axiomatization of all valid formulas has been given in [6].

In general, the calculation of $[S]p$ by means of a compositional analysis of
$p$, in contrast with the standard approach, does not generate additional
_nesting_ of the separating connectives. On the other hand, the compositional
analysis generates a case distinction in the definitions of $[\langle
x\rangle:=e](p\mathrel{*}q)$ and $[\langle
x\rangle:=\bot](p\mathrel{-\kern-1.99997pt*}q)$. How the combined application
of the two approaches works in practice needs to be further investigated. Such
an investigation will also involve the use of the modalities for the basic
instructions in the generation of the verification conditions of a program (as
is done for example in the KeY tool [1] for the verification of Java
programs), which allows to _postpone_ and _optimize_ their actual application.
For example, the equivalence

$[x:=e][\langle y\rangle:=e^{\prime}]p\equiv[\langle
y\rangle:=e^{\prime}[e/x]][x:=e]p$

allows to resolve the simple assignment modality by ‘pushing it inside’.

Other works that investigate weakest preconditions in SL are briefly discussed
below. For example, [3] investigates both weakest preconditions and strongest
postconditions in SL, also obtained through a transformational approach.
However, the transformation uses other separating connectives (like
_septraction_), and thus is not graceful. On the other hand, in [13] an
alternative logic is introduced which, instead of the separating connectives,
extends standard first-order logic with an operator ${\it Sp}(p)$ which
captures the parts of the heap the (first-order) formula $p$ depends on. Thus
also [13] goes beyond first-order, and is not graceful. But the main
motivation of that work coincides with ours: avoiding unnecessary reasoning
about the separating connectives.

Our artifact formalizes the syntax and semantics of programs and assertions of
SL. We plan to further extend our formalization to support practical program
verification, and investigate how to integrate our approach in Iris [11]: we
will consider how DSL can also work for a shallow embedding of SL. Then the
generated verification conditions require a proof of the validity of
corresponding assertions in SL, which can be discharged by providing a proof
directly in Coq. Further, we will investigate the application of DSL to
concurrent SL [4] and permission-based SL [2].

## References

  * [1] Ahrendt, W., B. Beckert, R. Bubel, R. Hähnle, P. H. Schmitt and M. Ulbrich, editors, “Deductive Software Verification - The KeY Book \- From Theory to Practice,” Lecture Notes in Computer Science 10001, Springer, 2016.
URL https://doi.org/10.1007/978-3-319-49812-6

  * [2] Amighi, A., C. Hurlin, M. Huisman and C. Haack, _Permission-based separation logic for multithreaded java programs_ , Logical Methods in Computer Science 11 (2015).
  * [3] Bannister, C., P. Höfner and G. Klein, _Backwards and forwards with separation logic_ , in: J. Avigad and A. Mahboubi, editors, _Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings_ , Lecture Notes in Computer Science 10895 (2018), pp. 68–87.
  * [4] Brookes, S. and P. W. O’Hearn, _Concurrent separation logic_ , ACM SIGLOG News 3 (2016), pp. 47–65.
  * [5] Charguéraud, A., _Separation logic for sequential programs (functional pearl)_ , Proc. ACM Program. Lang. 4 (2020).
URL https://doi.org/10.1145/3408998

  * [6] Demri, S., É. Lozes and A. Mansutti, _A complete axiomatisation for quantifier-free separation logic_ , Log. Methods Comput. Sci. 17 (2021).
URL https://doi.org/10.46298/lmcs-17(3:17)2021

  * [7] Dijkstra, E., “A Discipline of Programming,” Prentice-Hall, 1976.
  * [8] Faisal Al Ameen, M. and M. Tatsuta, _Completeness for recursive procedures in separation logic_ , Theoretical Computer Science 631 (2016), pp. 73–96.
URL https://www.sciencedirect.com/science/article/pii/S0304397516300329

  * [9] Harel, D., “First-Order Dynamic Logic,” Lecture Notes in Computer Science 68, Springer, 1979.
  * [10] Ishtiaq, S. S. and P. W. O’Hearn, _Bi as an assertion language for mutable data structures_ , SIGPLAN Not. 36 (2001), p. 14–26.
URL https://doi.org/10.1145/373243.375719

  * [11] Jung, R., R. Krebbers, J.-H. Jourdan, A. Bizjak, L. Birkedal and D. Dreyer, _Iris from the ground up: A modular foundation for higher-order concurrent separation logic_ , Journal of Functional Programming 28 (2018).
  * [12] Krebbers, R., Personal communication.
  * [13] Murali, A., L. Peña, C. Löding and P. Madhusudan, _A first-order logic with frames_ , in: P. Müller, editor, _Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings_ , Lecture Notes in Computer Science 12075 (2020), pp. 515–543.
  * [14] O’Connor, R., _Classical mathematics for a constructive world_ , Mathematical Structures in Computer Science 21 (2011), pp. 861–882.
  * [15] O’Hearn, P. W., J. C. Reynolds and H. Yang, _Local reasoning about programs that alter data structures_ , in: L. Fribourg, editor, _Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings_ , Lecture Notes in Computer Science 2142 (2001), pp. 1–19.
URL https://doi.org/10.1007/3-540-44802-0_1

  * [16] Reynolds, A., Personal communication.
  * [17] Reynolds, A., R. Iosif, C. Serban and T. King, _A decision procedure for separation logic in smt_ , in: _International Symposium on Automated Technology for Verification and Analysis_ , Springer, 2016, pp. 244–261.
  * [18] Reynolds, J. C., _Intuitionistic reasoning about shared mutable data structure_ , Millennial perspectives in computer science 2 (2000), pp. 303–321.
  * [19] Reynolds, J. C., _Separation logic: A logic for shared mutable data structures_ , in: _17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings_ (2002), pp. 55–74.
URL https://doi.org/10.1109/LICS.2002.1029817

  * [20] Sighireanu, M., J. A. Navarro Pérez, A. Rybalchenko, N. Gorogiannis, R. Iosif, A. Reynolds, C. Serban, J. Katelaan, C. Matheja, T. Noll et al., _Sl-comp: competition of solvers for separation logic_ , in: _International Conference on Tools and Algorithms for the Construction and Analysis of Systems_ , Springer, 2019, pp. 116–132.
  * [21] Tatsuta, M., W.-N. Chin and M. F. Al Ameen, _Completeness and expressiveness of pointer program verification by separation logic_ , Information and Computation 267 (2019), pp. 1–27.
URL https://www.sciencedirect.com/science/article/pii/S0890540119300203

  * [22] Vukmirović, P., J. Blanchette, S. Cruanes and S. Schulz, _Extending a brainiac prover to lambda-free higher-order logic_ , International Journal on Software Tools for Technology Transfer 24 (2022), pp. 67–87.
  * [23] Yang, H. and P. W. O’Hearn, _A semantic basis for local reasoning_ , in: _International Conference on Foundations of Software Science and Computation Structures_ , Springer, 2002, pp. 402–416.

##  Appendix A Appendix

$S\Coloneqq x:=[e]\mid[x]:=e\mid x:=\mbox{{\bf cons}}(e)\mid\mbox{{\bf
dispose}}(x)\mid$

$x:=e\mid S;S\mid\mbox{{\bf if}\ }b\mbox{\ {\bf then}\ }S\mbox{\ {\bf else}\
}S\mbox{\ {\bf fi}}\mid\mbox{{\bf while}\ }b\mbox{\ {\bf do}\ }S\mbox{\ {\bf
od}}$

$\langle x:=e,h,s\rangle\Rightarrow(h,s[x:=s(e)])$,

$\langle x:=[e],h,s\rangle\Rightarrow(h,s[x:=h(s(e))])$ if $s(e)\in\mbox{\it
dom}(h)$,

$\langle x:=[e],h,s\rangle\Rightarrow\mbox{\bf fail}$ if $s(e)\not\in\mbox{\it
dom}(h)$,

$\langle[x]:=e,h,s\rangle\Rightarrow(h[s(x):=s(e)],s)$ if $s(x)\in\mbox{\it
dom}(h)$,

$\langle[x]:=e,h,s\rangle\Rightarrow\mbox{\bf fail}$ if $s(x)\not\in\mbox{\it
dom}(h)$,

$\langle x:=\mbox{{\bf cons}}(e),h,s\rangle\Rightarrow(h[n:=s(e)],s[x:=n])$
where $n\not\in\mbox{\it dom}(h)$.

$\langle\mbox{{\bf dispose}}(x),h,s\rangle\Rightarrow(h[s(x):=\bot],s)$ if
$s(x)\in\mbox{\it dom}(h)$,

$\langle\mbox{{\bf dispose}}(x),h,s\rangle\Rightarrow\mbox{\bf fail}$ if
$s(x)\not\in\mbox{\it dom}(h)$,

$\langle S_{1};S_{2},h,s\rangle\Rightarrow o$ if $\langle
S_{1},h,s\rangle\Rightarrow(h^{\prime},s^{\prime})$ and $\langle
S_{2},h^{\prime},s^{\prime}\rangle\Rightarrow o$,

$\langle S_{1};S_{2},h,s\rangle\Rightarrow\mbox{\bf fail}$ if $\langle
S_{1},h,s\rangle\Rightarrow\mbox{\bf fail}$,

$\langle\mbox{{\bf if}\ }b\mbox{\ {\bf then}\ }S_{1}\mbox{\ {\bf else}\
}S_{2}\mbox{\ {\bf fi}},h,s\rangle\Rightarrow o$ if $s(b)=\mbox{{\bf true}}$
and $\langle S_{1},h,s\rangle\Rightarrow o$,

$\langle\mbox{{\bf if}\ }b\mbox{\ {\bf then}\ }S_{1}\mbox{\ {\bf else}\
}S_{2}\mbox{\ {\bf fi}},h,s\rangle\Rightarrow o$ if $s(b)=\mbox{{\bf false}}$
and $\langle S_{2},h,s\rangle\Rightarrow o$,

$\langle\mbox{{\bf while}\ }b\mbox{\ {\bf do}\ }S\mbox{\ {\bf
od}},h,s\rangle\Rightarrow o$ if $s(b)=\mbox{{\bf true}}$, $\langle
S,h,s\rangle\Rightarrow(h^{\prime},s^{\prime})$, and $\langle\mbox{{\bf
while}\ }b\mbox{\ {\bf do}\ }S\mbox{\ {\bf
od}},h^{\prime},s^{\prime}\rangle\Rightarrow o$,

$\langle\mbox{{\bf while}\ }b\mbox{\ {\bf do}\ }S\mbox{\ {\bf
od}},h,s\rangle\Rightarrow\mbox{\bf fail}$ if $s(b)=\mbox{{\bf true}}$ and
$\langle S,h,s\rangle\Rightarrow\mbox{\bf fail}$,

$\langle\mbox{{\bf while}\ }b\mbox{\ {\bf do}\ }S\mbox{\ {\bf
od}},h,s\rangle\Rightarrow(h,s)$ if $s(b)=\mbox{{\bf false}}$.

Figure 4: Syntax and semantics of heap manipulating programs.

$\\{{p}\\}\ {S}\ \\{{q}\\}\lx@proof@logical@and\models p\to
p^{\prime}\\{{p^{\prime}}\\}\ {S}\ \\{{q^{\prime}}\\}\models q^{\prime}\to q$
$\\{{p}\\}\ {S_{1};S_{2}}\ \\{{q}\\}\lx@proof@logical@and\\{{p}\\}\ {S_{1}}\
\\{{r}\\}\\{{r}\\}\ {S_{2}}\ \\{{q}\\}$ $\\{{p}\\}\ {\mbox{{\bf if}\ }b\mbox{\
{\bf then}\ }S_{1}\mbox{\ {\bf else}\ }S_{2}\mbox{\ {\bf fi}}}\
\\{{q}\\}\lx@proof@logical@and\\{{p\land b}\\}\ {S_{1}}\
\\{{q}\\}\\{{p\land\lnot b}\\}\ {S_{2}}\ \\{{q}\\}$ $\\{{p}\\}\ {\mbox{{\bf
while}\ }b\mbox{\ {\bf do}\ }S\mbox{\ {\bf od}}}\ \\{{p\land\lnot
b}\\}\\{{p\land b}\\}\ {S}\ \\{{p}\\}$

Figure 5: Hoare’s standard proof rules.

${\\{{p}\\}\ {x:=e}\ \\{{\exists y(p[x:=y]\land x=e[x:=y])}\\}}{}$
${\\{{p\wedge(e\hookrightarrow-)}\\}\ {x:=[e]}\ \\{{(e\mapsto
x)\mathrel{*}\lnot((e\mapsto x)\mathrel{-\kern-1.99997pt*}\lnot p)}\\}}$
${\\{{p\wedge(x\hookrightarrow-)}\\}\ {[x]:=e}\ \\{{(x\mapsto
e)\mathrel{*}\lnot((x\mapsto-)\mathrel{-\kern-1.99997pt*}\lnot p)}\\}}{}$
${\\{{p}\\}\ {x:=\mbox{{\bf cons}}(e)}\ \\{{(x\mapsto e)\mathrel{*}p}\\}}{}$
${\\{{p\wedge(x\hookrightarrow-)}\\}\ {\mbox{{\bf dispose}}(x)}\
\\{{\lnot((x\mapsto-)\mathrel{-\kern-1.99997pt*}\lnot p)}\\}}$

Figure 6: Global strongest postcondition axiomatization (cf. [19, 3]),
assuming $x$ does not occur in $e$ in the axioms for look-up, mutation, and
allocation.