Systematic Design of Separation Logics

Lorenzo Gazzella; Roberta Gori; Roberto Bruni

arxiv: 2605.21262 · v1 · pith:2LWTHTA5new · submitted 2026-05-20 · 💻 cs.LO

Systematic Design of Separation Logics

Roberto Bruni , Lorenzo Gazzella , Roberta Gori This is my paper

Pith reviewed 2026-05-21 03:47 UTC · model grok-4.3

classification 💻 cs.LO

keywords separation logiclocal axiomsframe rulesheap manipulationprogram semanticscalculational designabstract interpretation

0 comments

The pith

A parametric methodology derives local axioms for separation logics by exploiting semantic closure properties to embed locality by construction.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes a general methodology for systematically deriving local axioms in separation logics where the locality principle is embedded by construction. This is achieved by leveraging semantic closure properties to calculate the minimal required heap for heap-manipulating primitives and their corresponding pre- and postconditions. The method also generates universal frame rules without additional syntactic side conditions. It is designed to be parametric with respect to these properties, allowing it to handle different memory models and to reuse inference rules across over- and under-approximations. As a result, the produced logical systems can derive a broader range of triples than existing program logics for correctness and incorrectness analyses, including a demonstration for inferring necessary preconditions.

Core claim

The central claim is that by exploiting a suitable set of semantic closure properties, one can parametrically derive local axioms for separation logics. For heap-manipulating primitives, this yields the minimal required heap along with pre- and postconditions, and complements them with universal frame rules that require no additional syntactic side conditions. The method works for various memory models and favors reuse of rules between different approximation directions, enabling proof systems that cover more triples than previous ones like Separation Logic and Incorrectness Separation Logic.

What carries the argument

Parametric derivation of local axioms from semantic closure properties, which by construction ensures only the minimal heap is referenced and provides universal frame rules.

If this is right

Local axioms are generated automatically for any heap primitive once closure properties are fixed.
Frame rules apply universally without needing per-axiom syntactic conditions.
Inference rules are reusable when moving from over-approximation to under-approximation or vice versa.
The resulting systems prove a wider set of triples than hand-designed alternatives for (in)correctness.
A proof system for necessary preconditions can be obtained by applying the same methodology.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

This methodology might enable tool builders to add support for new memory models by simply identifying the relevant closure properties rather than redesigning axioms.
It could lead to more consistent verification frameworks that handle both correctness and incorrectness with minimal additional effort.
Extensions to programs with concurrency or other features would require identifying appropriate closure properties for those settings.

Load-bearing premise

The approach depends on being able to identify and use appropriate semantic closure properties for the specific memory model and analysis direction.

What would settle it

If no set of semantic closure properties can be found that produces local axioms for a given heap-manipulating language, or if the derived axioms fail to validate triples known to be valid under separation logic, the systematic derivation would not hold.

Figures

Figures reproduced from arXiv: 2605.21262 by Lorenzo Gazzella, Roberta Gori, Roberto Bruni.

**Figure 1.** Figure 1: Semantic proof systems. The figure is divided into four groups. First, we list the rules for axioms, according to Corollary 4.4. In the second group, we list rules induced by closure operators (for Disj see Section 4.2.1). The third group collects standard rules for command compositions, while auxiliary rules are in the fourth group. Key novelties are in light blue. Except for the new transfer and frame ru… view at source ↗

**Figure 2.** Figure 2: SL+: Synthesized axioms for forward correctness analysis in both memory models [PITH_FULL_IMAGE:figures/full_fig_p017_2.png] view at source ↗

**Figure 3.** Figure 3: ISL+: Synthesized axioms for forward incorrectness analysis in both memory models [PITH_FULL_IMAGE:figures/full_fig_p020_3.png] view at source ↗

**Figure 4.** Figure 4: SIL+: Synthesized axioms for backward incorrectness analysis in both memory models [PITH_FULL_IMAGE:figures/full_fig_p024_4.png] view at source ↗

**Figure 5.** Figure 5: NC+: Synthesized proof system for backward correctness analysis in both memory models [PITH_FULL_IMAGE:figures/full_fig_p025_5.png] view at source ↗

**Figure 6.** Figure 6: The SL denotational semantics [Reynolds 2002] [PITH_FULL_IMAGE:figures/full_fig_p031_6.png] view at source ↗

**Figure 7.** Figure 7: The ISL denotational semantics [Raad et al. 2020] [PITH_FULL_IMAGE:figures/full_fig_p032_7.png] view at source ↗

**Figure 8.** Figure 8: SL+: Synthesized proof system for forward correctness analysis in both memory models [PITH_FULL_IMAGE:figures/full_fig_p033_8.png] view at source ↗

**Figure 9.** Figure 9: ISL+: Synthesized proof system for forward incorrectness analysis in both memory models [PITH_FULL_IMAGE:figures/full_fig_p034_9.png] view at source ↗

**Figure 10.** Figure 10: Additional rules for parallel composition in CISL+. [PITH_FULL_IMAGE:figures/full_fig_p034_10.png] view at source ↗

**Figure 11.** Figure 11: SIL+: Synthesized proof system for backward incorrectness analysis in both memory models [PITH_FULL_IMAGE:figures/full_fig_p035_11.png] view at source ↗

**Figure 12.** Figure 12: A sample derivation in SL+ showing that it is more expressive than SL: the triple [PITH_FULL_IMAGE:figures/full_fig_p047_12.png] view at source ↗

**Figure 13.** Figure 13: A sample derivation in ISL+ showing that it is more expressive than ISL: the triple [PITH_FULL_IMAGE:figures/full_fig_p048_13.png] view at source ↗

read the original abstract

Thanks to the locality principle, separation logics support modular, scalable analysis of large codebases by relying on local axioms and frame rules to focus only on the heap fragments required for verification. However, depending on the direction (forward vs. backward) and sense of approximation (over vs. under) of the analysis, designing the corresponding proof systems can require some ingenuity. In his work on the calculational design of program logics, Patrick Cousot outlines a methodology for deriving proof systems directly from program semantics using abstract interpretation, covering both correctness and incorrectness analyses. Unfortunately, when applied to heap-manipulating programs, Cousot's calculational approach cannot handle the locality principle, because it does not provide a calculational way to derive frame rules and produces axioms that refer to the global heap. In this paper, we propose a general methodology for systematically deriving local axioms in which the locality principle is embedded by construction. For heap-manipulating primitives, we can derive the minimal required heap and the corresponding pre- and postconditions, complemented by universal frame rules without additional syntactic side conditions. Our method is parametric w.r.t. a set of semantic closure properties that are exploited to design local axioms; it can deal with different memory models; it favors the reuse of many inference rules across over- and under-approximation; and it produces logical systems capable of deriving a broader range of triples w.r.t. existing, cleverly designed, program logics for (in)correctness, ranging from Separation Logic and Incorrectness Separation Logic to Separation Sufficient Incorrectness Logic. Furthermore, we demonstrate the flexibility of our methodology by applying it to design a novel proof system for inferring necessary preconditions with separation logic.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives a parametric way to derive local separation logic axioms and universal frame rules from semantics by exploiting closure properties, extending Cousot's calculational design to handle locality by construction.

read the letter

The core contribution is a general template that starts from program semantics and uses a set of closure properties to produce axioms that only mention the minimal heap fragment needed, plus frame rules that apply without extra syntactic conditions. This covers forward and backward reasoning, over- and under-approximation, and reuses many rules across those directions. They apply it to standard heap primitives and also sketch a new system for necessary preconditions in separation logic, which goes beyond the usual correctness and incorrectness logics they cite. That reuse and the broader set of derivable triples are the practical upsides if the method works as described. The approach is explicitly parametric on the closure properties, which is meant to let it adapt to different memory models without starting from scratch each time. If the paper supplies clear recipes or examples for identifying those properties on common operations like allocation or field updates, it could reduce the ad-hoc design work that usually goes into separation logics. The main soft spot is whether those properties can be found and checked systematically or whether they still demand comparable ingenuity to the original axiom design. The abstract flags this dependency, so the paper needs to show that the extra step is lighter than hand-crafting locality rules on top of Cousot-style derivations. Without concrete derivations or a worked example that makes the property selection look mechanical, it is hard to judge how much the calculational advantage actually materializes. This is for people who build or extend program logics for heap programs and want a more uniform way to obtain local reasoning principles. Readers already familiar with Cousot's abstract-interpretation work or with the design of Separation Logic and Incorrectness Separation Logic will see the most direct value. It deserves a serious referee because the problem it targets is real and the parametric framing is a substantive shift from prior per-logic cleverness, even if the details of the closure properties need careful checking.

Referee Report

2 major / 2 minor

Summary. The paper proposes a general methodology for systematically deriving local axioms in separation logics, embedding the locality principle by construction via semantic closure properties. For heap-manipulating primitives, it derives the minimal required heap along with corresponding pre- and postconditions, plus universal frame rules without syntactic side conditions. The approach is parametric on a set of semantic closure properties, handles different memory models and analysis directions (over/under-approximation, forward/backward), reuses inference rules across variants, and produces systems capable of deriving broader triples than existing logics such as Separation Logic, Incorrectness Separation Logic, and Separation Sufficient Incorrectness Logic. It is also applied to design a novel proof system for inferring necessary preconditions.

Significance. If the derivations hold, the work offers a calculational route to locality-aware proof systems that avoids per-case ingenuity, potentially enabling reuse across correctness and incorrectness analyses and supporting new logics such as the necessary-precondition variant. The parametric treatment of closure properties and explicit handling of minimal heaps are strengths that could reduce manual design effort in separation-logic variants.

major comments (2)

[§4.1, Definition 4.3] §4.1, Definition 4.3: the claim that the methodology is 'systematic' and 'parametric' requires that the closure properties be identifiable without ingenuity comparable to hand-crafting axioms; the paper should state a precise criterion for when a set of closure properties is 'suitable' and prove that such sets exist for the standard heap primitives considered (allocation, deallocation, mutation).
[§5.3, Theorem 5.7] §5.3, Theorem 5.7: the derivation of the universal frame rule is shown to hold without side conditions, but the proof sketch relies on the closure properties being preserved under the memory model; an explicit check that the properties survive the transition from global to local heap semantics would strengthen the result.

minor comments (2)

[§3] Notation for the minimal heap fragment is introduced in §3 but used without reminder in later examples; a short table summarizing the derived pre/postconditions for each primitive would improve readability.
[§6] The comparison in §6 with Cousot-style derivation would benefit from a side-by-side example showing where the closure-property step replaces a manual locality patch.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the positive evaluation and the insightful comments. We respond to each major comment below.

read point-by-point responses

Referee: [§4.1, Definition 4.3] §4.1, Definition 4.3: the claim that the methodology is 'systematic' and 'parametric' requires that the closure properties be identifiable without ingenuity comparable to hand-crafting axioms; the paper should state a precise criterion for when a set of closure properties is 'suitable' and prove that such sets exist for the standard heap primitives considered (allocation, deallocation, mutation).

Authors: We agree that a precise criterion for suitable closure properties would make the systematic character of the methodology more explicit. In the manuscript the closure properties are obtained directly by inspecting the semantic definitions of the primitives, and concrete sets are supplied for allocation, deallocation and mutation. To address the referee's point we will revise Definition 4.3 to introduce a formal notion of suitability and add a short proposition establishing that the sets employed for the standard heap primitives satisfy the criterion. revision: yes
Referee: [§5.3, Theorem 5.7] §5.3, Theorem 5.7: the derivation of the universal frame rule is shown to hold without side conditions, but the proof sketch relies on the closure properties being preserved under the memory model; an explicit check that the properties survive the transition from global to local heap semantics would strengthen the result.

Authors: We thank the referee for this observation. The proof of Theorem 5.7 is parametric and the preservation of the closure properties follows from their semantic definition, yet we accept that an explicit verification would improve clarity. In the revised version we will extend the proof sketch in §5.3 with a direct argument showing that the relevant closure properties are preserved when moving from the global to the local heap semantics for the memory models considered. revision: yes

Circularity Check

0 steps flagged

Methodology derives local axioms parametrically from external semantic closure properties

full rationale

The paper's derivation begins from program semantics via abstract interpretation (Cousot-style) and a parametric set of semantic closure properties that are supplied as input to obtain local axioms and universal frame rules. No step reduces the output axioms to the input axioms by definition or construction; the closure properties are external semantic facts about the memory model and primitives, not derived from the target logic. The abstract and description emphasize generality across models and analysis directions without self-referential definitions, fitted parameters renamed as predictions, or load-bearing self-citations. The central claim remains independent of the specific axioms produced and is falsifiable against different memory models or primitives lacking the required closure properties.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the availability of semantic closure properties that enable the parametric derivation of local axioms; these properties are treated as given inputs rather than derived within the paper.

axioms (1)

domain assumption A suitable set of semantic closure properties exists for the program semantics under consideration.
The methodology is explicitly parametric with respect to these properties to design the local axioms.

pith-pipeline@v0.9.0 · 5832 in / 1322 out tokens · 36115 ms · 2026-05-21T03:47:52.151308+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

Our method is parametric w.r.t. a set of semantic closure properties... complemented by universal frame rules without additional syntactic side conditions.
IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean absolute_floor_iff_bare_distinguishability unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We exploit semantic closure properties to derive the minimal set of axioms...

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

12 extracted references · 12 canonical work pages

[1]

By definition of JrK and (3), we have that (𝑠, ℎ′

∈J rK{(𝑠 ′, ℎ1)} with ℎ=ℎ ′ 1 •ℎ 2. By definition of JrK and (3), we have that (𝑠, ℎ′

work page
[2]

Finally, by (4) and the hypothesis of 𝑅∈F , we have that (𝑠, ℎ2) ∈𝑅 , and so by hypothesis 𝑃 ▶ ◀𝑅 we have that ℎ′ 1#ℎ2

∈J rK𝑃. Finally, by (4) and the hypothesis of 𝑅∈F , we have that (𝑠, ℎ2) ∈𝑅 , and so by hypothesis 𝑃 ▶ ◀𝑅 we have that ℎ′ 1#ℎ2. Hence (𝑠, ℎ′ 1 •ℎ 2) ∈𝑄•𝑅 , which is(𝑠, ℎ ′ 1 •ℎ 2) ∈𝑄•𝑅sinceℎ=ℎ ′ 1 •ℎ 2.□ Theorem 4.2 (Backward Semantic Preservation).Given 𝑃, r, 𝑄 such that J← −rK𝑄=𝑃 and 𝑅∈F such that𝑄 ▶ ◀𝑅, then(J ← −rK𝑄) •𝑅=J ← −rK(𝑄•𝑅)=𝑃•𝑅. Proof.Analogo...

work page 1978
[3]

ˆMi ∗M ′ for someM ′

∨ (a ′ 3∗k ′ 1 ̸↦→) Lemma D.1.Each assertionM i can be rewritten in a normal form∃a ′. ˆMi ∗M ′ for someM ′. Proof. We only show the proof for memory model 2 since it includes the case for memory model1 . We proceed by induction on the structure ofM 2, using the letterPfor pure assertions: CaseM 2 ≜P: We rewriteP≡ ∃a ′. ˆM2 ∗P and we prove the equivalence...

work page
[4]

ˆM2 ∗H ′ 1 andH 2 ≡ ∃a ′

∨ (H ′ 1 ∗H 2)) with H1 ≡ ∃a ′. ˆM2 ∗H ′ 1 andH 2 ≡ ∃a ′. ˆM2 ∗H ′ 2. The first three equivalences are trivial, so we only prove (4): ⇒) Suppose (𝑠, ℎ) ∈ { |H1 ∗H 2| }. By definition of ∗, there exists ℎ1, ℎ2 s.t. ℎ=ℎ 1 •ℎ 2, (𝑠, ℎ1) ∈ { |H1| } and (𝑠, ℎ2) ∈ { |H2| }. By definition of H1 and H2 we have (𝑠, ℎ1) ∈ { |∃a′. ˆM2 ∗H ′ 1| }and (𝑠, ℎ2) ∈ { |∃a′. ...

work page
[5]

∈ { |ˆM2| }, (𝑠, ℎ′′ 1 ) ∈ { |H′ 1| }, (𝑠, ℎ′

work page
[6]

Then (𝑠, ℎ′ 1 • ℎ′′ 1 •ℎ 2) ∈ { |ˆM2 ∗H ′ 1 ∗H 2| }and so also (𝑠, ℎ′ 1 •ℎ ′′ 1 •ℎ 2) ∈ { |∃a′

∈ { |ˆM2| }, (𝑠, ℎ′′ 2 ) ∈ { |H′ 2| }. Then (𝑠, ℎ′ 1 • ℎ′′ 1 •ℎ 2) ∈ { |ˆM2 ∗H ′ 1 ∗H 2| }and so also (𝑠, ℎ′ 1 •ℎ ′′ 1 •ℎ 2) ∈ { |∃a′. ˆM2 ∗H ′ 1 ∗H 2| }. Furthermore, (𝑠, ℎ1 •ℎ ′ 2 •ℎ ′′ 2 ) ∈ { |H1 ∗ ˆM2 ∗H ′ 2| }and so also(𝑠, ℎ 1 •ℎ ′ 2 •ℎ ′′ 2 ) ∈ { |∃a′.H1 ∗ ˆM2 ∗H ′ 2| }. Systematic Design of Separation Logics 43 ⇐) Suppose (𝑠, ℎ) ∈ { |∃a′. ˆM2 ∗ (...

work page
[7]

By definition of ∗ and ∃, there exists 𝑣, ℎ1, ℎ2 s.t

∨ (H ′ 1 ∗H 2)) | }. By definition of ∗ and ∃, there exists 𝑣, ℎ1, ℎ2 s.t. ℎ=ℎ 1•ℎ2, (𝑠[a ′ ↦→𝑣], ℎ 1) ∈ { |ˆM2| }and (𝑠[a ′ ↦→𝑣], ℎ 2) ∈ { |(H1 ∗H ′

work page
[8]

We proceed by case on the disjuncts of the assertion(H 1 ∗H ′

∨ (H ′ 1 ∗H 2)| }. We proceed by case on the disjuncts of the assertion(H 1 ∗H ′

work page
[9]

Then by definition of ∗ there exists ℎ′ 2, ℎ′′ 2 s.t

∨ (H ′ 1 ∗H 2): • Suppose (𝑠[a ′ ↦→𝑣], ℎ 2) ∈ { |H1 ∗H ′ 2| }. Then by definition of ∗ there exists ℎ′ 2, ℎ′′ 2 s.t. (𝑠[a ′ ↦→𝑣], ℎ ′

work page
[10]

Then (𝑠[a ′ ↦→𝑣], ℎ 1•ℎ ′′ 2 ) ∈ { |H2| }

∈ { |H1| }and (𝑠[a ′ ↦→𝑣], ℎ ′′ 2 ) ∈ { |H′ 2| }. Then (𝑠[a ′ ↦→𝑣], ℎ 1•ℎ ′′ 2 ) ∈ { |H2| }. Then(𝑠[a ′ ↦→𝑣], ℎ 1 •ℎ ′ 2 •ℎ ′′ 2 ) ∈ { |H1 ∗H 2| }. •The other case is dual. CaseM 2 ≜P∧H 2: By inductive hypothesisH 2 ≡ ∃a ′. ˆM2 ∗H ′, then we rewriteP∧H 2 ≡ ∃a ′. ˆM2 ∗P∧H ′: P∧H 2 ≡P∧ ∃a ′. ˆM2 ∗H ′ ≡ ∃a ′.P∧ ˆM2 ∗H ′ ≡ ∃a ′. ˆM2 ∗P∧H ′ where we used the f...

work page
[11]

ˆM2 ∗ (M ′ 1 ∨M ′ 2) where we used the distributivity of the∗over∨

≡ ∃a ′. ˆM2 ∗ (M ′ 1 ∨M ′ 2) where we used the distributivity of the∗over∨. CaseM 2 ≜∃X.M 1: By inductive hypothesisM 1 ≡ ∃a ′. ˆM2 ∗M ′ 1, then we rewrite∃X.M 1 ≡ ∃a ′. ˆM2 ∗ (∃X.M ′ 1): ∃X.M1 ≡ ∃X.(∃a ′. ˆM2 ∗M ′

work page
[12]

ˆM2 ∗M ′ 1 ≡ ∃a ′

≡ ∃a ′.∃X. ˆM2 ∗M ′ 1 ≡ ∃a ′. ˆM2 ∗ (∃X.M ′ 1) □ Lemma D.2.We can rewrite ˆM1 and ˆM2 in the following forms: (1) ˆM1 ≡ H∗ ˆMwith H=emp (2) ˆM2 ≡ H∗ ˆM2 with H=emp (3) ˆM2 ≡ H∗ (emp∨ (a 3∗k 1 ̸↦→))with H=((a 1∗emp) ∨ (a 2∗k 1 ↦→k 2)) Theorem 5.1 (SL+ Sound and Relative Complete for Loop-Free Programs).Let r∈Reg and P,Q∈Ast , then ⊢i SL+ {P} r {Q} ⇒J rKSL ...

work page

[1] [1]

By definition of JrK and (3), we have that (𝑠, ℎ′

∈J rK{(𝑠 ′, ℎ1)} with ℎ=ℎ ′ 1 •ℎ 2. By definition of JrK and (3), we have that (𝑠, ℎ′

work page

[2] [2]

Finally, by (4) and the hypothesis of 𝑅∈F , we have that (𝑠, ℎ2) ∈𝑅 , and so by hypothesis 𝑃 ▶ ◀𝑅 we have that ℎ′ 1#ℎ2

∈J rK𝑃. Finally, by (4) and the hypothesis of 𝑅∈F , we have that (𝑠, ℎ2) ∈𝑅 , and so by hypothesis 𝑃 ▶ ◀𝑅 we have that ℎ′ 1#ℎ2. Hence (𝑠, ℎ′ 1 •ℎ 2) ∈𝑄•𝑅 , which is(𝑠, ℎ ′ 1 •ℎ 2) ∈𝑄•𝑅sinceℎ=ℎ ′ 1 •ℎ 2.□ Theorem 4.2 (Backward Semantic Preservation).Given 𝑃, r, 𝑄 such that J← −rK𝑄=𝑃 and 𝑅∈F such that𝑄 ▶ ◀𝑅, then(J ← −rK𝑄) •𝑅=J ← −rK(𝑄•𝑅)=𝑃•𝑅. Proof.Analogo...

work page 1978

[3] [3]

ˆMi ∗M ′ for someM ′

∨ (a ′ 3∗k ′ 1 ̸↦→) Lemma D.1.Each assertionM i can be rewritten in a normal form∃a ′. ˆMi ∗M ′ for someM ′. Proof. We only show the proof for memory model 2 since it includes the case for memory model1 . We proceed by induction on the structure ofM 2, using the letterPfor pure assertions: CaseM 2 ≜P: We rewriteP≡ ∃a ′. ˆM2 ∗P and we prove the equivalence...

work page

[4] [4]

ˆM2 ∗H ′ 1 andH 2 ≡ ∃a ′

∨ (H ′ 1 ∗H 2)) with H1 ≡ ∃a ′. ˆM2 ∗H ′ 1 andH 2 ≡ ∃a ′. ˆM2 ∗H ′ 2. The first three equivalences are trivial, so we only prove (4): ⇒) Suppose (𝑠, ℎ) ∈ { |H1 ∗H 2| }. By definition of ∗, there exists ℎ1, ℎ2 s.t. ℎ=ℎ 1 •ℎ 2, (𝑠, ℎ1) ∈ { |H1| } and (𝑠, ℎ2) ∈ { |H2| }. By definition of H1 and H2 we have (𝑠, ℎ1) ∈ { |∃a′. ˆM2 ∗H ′ 1| }and (𝑠, ℎ2) ∈ { |∃a′. ...

work page

[5] [5]

∈ { |ˆM2| }, (𝑠, ℎ′′ 1 ) ∈ { |H′ 1| }, (𝑠, ℎ′

work page

[6] [6]

Then (𝑠, ℎ′ 1 • ℎ′′ 1 •ℎ 2) ∈ { |ˆM2 ∗H ′ 1 ∗H 2| }and so also (𝑠, ℎ′ 1 •ℎ ′′ 1 •ℎ 2) ∈ { |∃a′

∈ { |ˆM2| }, (𝑠, ℎ′′ 2 ) ∈ { |H′ 2| }. Then (𝑠, ℎ′ 1 • ℎ′′ 1 •ℎ 2) ∈ { |ˆM2 ∗H ′ 1 ∗H 2| }and so also (𝑠, ℎ′ 1 •ℎ ′′ 1 •ℎ 2) ∈ { |∃a′. ˆM2 ∗H ′ 1 ∗H 2| }. Furthermore, (𝑠, ℎ1 •ℎ ′ 2 •ℎ ′′ 2 ) ∈ { |H1 ∗ ˆM2 ∗H ′ 2| }and so also(𝑠, ℎ 1 •ℎ ′ 2 •ℎ ′′ 2 ) ∈ { |∃a′.H1 ∗ ˆM2 ∗H ′ 2| }. Systematic Design of Separation Logics 43 ⇐) Suppose (𝑠, ℎ) ∈ { |∃a′. ˆM2 ∗ (...

work page

[7] [7]

By definition of ∗ and ∃, there exists 𝑣, ℎ1, ℎ2 s.t

∨ (H ′ 1 ∗H 2)) | }. By definition of ∗ and ∃, there exists 𝑣, ℎ1, ℎ2 s.t. ℎ=ℎ 1•ℎ2, (𝑠[a ′ ↦→𝑣], ℎ 1) ∈ { |ˆM2| }and (𝑠[a ′ ↦→𝑣], ℎ 2) ∈ { |(H1 ∗H ′

work page

[8] [8]

We proceed by case on the disjuncts of the assertion(H 1 ∗H ′

∨ (H ′ 1 ∗H 2)| }. We proceed by case on the disjuncts of the assertion(H 1 ∗H ′

work page

[9] [9]

Then by definition of ∗ there exists ℎ′ 2, ℎ′′ 2 s.t

∨ (H ′ 1 ∗H 2): • Suppose (𝑠[a ′ ↦→𝑣], ℎ 2) ∈ { |H1 ∗H ′ 2| }. Then by definition of ∗ there exists ℎ′ 2, ℎ′′ 2 s.t. (𝑠[a ′ ↦→𝑣], ℎ ′

work page

[10] [10]

Then (𝑠[a ′ ↦→𝑣], ℎ 1•ℎ ′′ 2 ) ∈ { |H2| }

∈ { |H1| }and (𝑠[a ′ ↦→𝑣], ℎ ′′ 2 ) ∈ { |H′ 2| }. Then (𝑠[a ′ ↦→𝑣], ℎ 1•ℎ ′′ 2 ) ∈ { |H2| }. Then(𝑠[a ′ ↦→𝑣], ℎ 1 •ℎ ′ 2 •ℎ ′′ 2 ) ∈ { |H1 ∗H 2| }. •The other case is dual. CaseM 2 ≜P∧H 2: By inductive hypothesisH 2 ≡ ∃a ′. ˆM2 ∗H ′, then we rewriteP∧H 2 ≡ ∃a ′. ˆM2 ∗P∧H ′: P∧H 2 ≡P∧ ∃a ′. ˆM2 ∗H ′ ≡ ∃a ′.P∧ ˆM2 ∗H ′ ≡ ∃a ′. ˆM2 ∗P∧H ′ where we used the f...

work page

[11] [11]

ˆM2 ∗ (M ′ 1 ∨M ′ 2) where we used the distributivity of the∗over∨

≡ ∃a ′. ˆM2 ∗ (M ′ 1 ∨M ′ 2) where we used the distributivity of the∗over∨. CaseM 2 ≜∃X.M 1: By inductive hypothesisM 1 ≡ ∃a ′. ˆM2 ∗M ′ 1, then we rewrite∃X.M 1 ≡ ∃a ′. ˆM2 ∗ (∃X.M ′ 1): ∃X.M1 ≡ ∃X.(∃a ′. ˆM2 ∗M ′

work page

[12] [12]

ˆM2 ∗M ′ 1 ≡ ∃a ′

≡ ∃a ′.∃X. ˆM2 ∗M ′ 1 ≡ ∃a ′. ˆM2 ∗ (∃X.M ′ 1) □ Lemma D.2.We can rewrite ˆM1 and ˆM2 in the following forms: (1) ˆM1 ≡ H∗ ˆMwith H=emp (2) ˆM2 ≡ H∗ ˆM2 with H=emp (3) ˆM2 ≡ H∗ (emp∨ (a 3∗k 1 ̸↦→))with H=((a 1∗emp) ∨ (a 2∗k 1 ↦→k 2)) Theorem 5.1 (SL+ Sound and Relative Complete for Loop-Free Programs).Let r∈Reg and P,Q∈Ast , then ⊢i SL+ {P} r {Q} ⇒J rKSL ...

work page