Editing Frame problem (section)

=== Separation logic solution ===
[[Separation logic]] is a formalism for reasoning about computer programs using pre/post specifications of the form <math>\{\mathrm{precondition}\}\ \mathrm{code}\ \{\mathrm{postcondition}\}</math>. Separation logic is an extension of [[Hoare logic]] oriented to  reasoning about mutable data structures in computer memory and other dynamic resources, and it has a special connective *, pronounced "and separately", to support independent reasoning about disjoint memory regions.<ref>{{Cite book|last=Reynolds|first=J.C.|title=Proceedings 17th Annual IEEE Symposium on Logic in Computer Science |chapter=Separation logic: A logic for shared mutable data structures |date=2002|location=Copenhagen, Denmark|publisher=IEEE Comput. Soc|pages=55–74|doi=10.1109/LICS.2002.1029817|citeseerx=10.1.1.110.7749|isbn=978-0-7695-1483-3|s2cid=6271346}}</ref><ref>{{Cite journal|last=O'Hearn|first=Peter|date=2019-01-28|title=Separation logic|journal=[[Communications of the ACM]]|language=en|volume=62|issue=2|pages=86–95|doi=10.1145/3211968|issn=0001-0782|doi-access=free}}</ref>

Separation logic employs a ''tight'' interpretation of pre/post specs, which say that the code can ''only'' access memory locations guaranteed to exist by the precondition.<ref>{{Cite book|last1=O’Hearn|first1=Peter|last2=Reynolds|first2=John|last3=Yang|first3=Hongseok|date=2001|editor-last=Fribourg|editor-first=Laurent|chapter=Local Reasoning about Programs that Alter Data Structures|title=Computer Science Logic|volume=2142|series=Lecture Notes in Computer Science|language=en|location=Berlin, Heidelberg|publisher=Springer|pages=1–19|doi=10.1007/3-540-44802-0_1|isbn=978-3-540-44802-0}}</ref> This leads to the soundness of the most important inference rule of the logic, the ''frame rule''

<math>\frac{ \{\mathrm{precondition}\}\ \mathrm{code}\ \{\mathrm{postcondition}\} }{ \{\mathrm{precondition} \ast \mathrm{frame}\}\ \mathrm{code}\ \{\mathrm{postcondition} \ast \mathrm{frame}\} }</math>

The frame rule  allows descriptions of arbitrary memory outside the footprint (memory accessed) of the code to be added to a specification: this enables the initial specification to concentrate only on the footprint.  For example, the inference

<math>\frac{ \{\operatorname{list}(x)\}\ \mathrm{code}\ \{\operatorname{sortedlist}(x)\} }{ \{\operatorname{list}(x) \ast \operatorname{sortedlist}(y)\}\ \mathrm{code}\ \{\operatorname{sortedlist}(x) \ast \operatorname{sortedlist}(y)\} }</math>

captures that code which sorts a list ''x'' does not unsort a separate list ''y,'' and it does this without mentioning ''y'' at all in the initial spec above the line.

Automation of the frame rule has led to significant increases in the scalability of automated reasoning techniques for code,<ref>{{Cite journal|last1=Calcagno Cristiano|last2=Dino Distefano|last3=Peter O'Hearn|last4=Hongseok Yang|date=2011-12-01|title=Compositional Shape Analysis by Means of Bi-Abduction|journal=[[Journal of the ACM]]|language=EN|volume=58|issue=6|pages=1–66|doi=10.1145/2049697.2049700|s2cid=52808268|url=https://ora.ox.ac.uk/objects/uuid:bcfefe74-a79c-4155-8160-c51f92f05466}}</ref> eventually deployed industrially to codebases with tens of millions of lines.<ref>{{Cite journal|first1=Dino |last1=Distefano|first2=Manuel |last2=Fähndrich|first3=Francesco |last3=Logozzo|first4=Peter |last4=O'Hearn|date=2019-07-24|title=Scaling static analyses at Facebook|journal=Communications of the ACM|language=EN|volume=62|issue=8|pages=62–70|doi=10.1145/3338112|doi-access=free}}</ref>

There appears to be some similarity between the separation logic solution to the frame problem and that of the fluent calculus mentioned above.{{explain|date=May 2022}}