A simple rationale for this stuff

In 2002, John C. Reynolds from CMU published a seminal work called Separation Logic: A Logic for Shared Mutable Data Structures. The very notion behind this logic is that some programming languages allow programmer to manually manage the memory. For example, C/C++ contains commands for accessing, modifying shared structures, allocating and deallocating memories. Assertions are extended by introducing a “separating conjunction” that asserts that its sub-formulas hold for disjoint parts of the heap, and a closely related “separating implication”.

Hoare Logic???

Yes, separation logic is an extension of Hoare logic, used for reasoning about assertions about programs that access and mutate data held in (shared) computer memory. It is “separate” in a sense that it is baed on separating conjunction $P * Q$ which asserts that $P$ and $Q$ holds for separate portions of memory and allows on the modularly describe states of a program Marktoberdorf11LectureNotes.pdf (ucl.ac.uk).

In general, an assertion $P$ denotes a set of states, and $P ∗ Q$ is true of a state just if its heap/RAM component can be split into two parts, one of which satisfies $P$ and the other of which satisfies $Q$.

Formally:

• $emp$: The heap is empty.
• $x \mapsto y$: The heap contains a pointer $x$ that points to $y$.
• $P * Q$: The heap can be split into two disjunctive parts where $P$ and $Q$ hold for these two parts.

A separation logic tuple: $\{ P \} C \{ Q \}$.