Бөлу логикасы: программаларды дәлелдеудің кеңейтілген әдісі

In computer science, separation logic is an extension of Hoare logic, a way of reasoning about programs. It was developed by John C. Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang, drawing upon early work by Rod Burstall. The assertion language of separation logic is a special case of the logic of bunched implications (BI). A CACM review article by O'Hearn charts developments in the subject to early 2019.

Separation logic assertions describe "states" consisting of a store and a heap, roughly corresponding to the state of local (or stack allocated) variables and dynamically allocated objects in common programming languages such as C and Java. A store is a function mapping variables to values. A heap is a partial function mapping memory addresses to values. Two heaps and are disjoint (denoted ) if their domains do not overlap (i. e., for every memory address , at least one of and is undefined). The logic allows to prove judgements of the form , where is a store, is a heap, and is an assertion over the given store and heap. Separation logic assertions (denoted as , , ) contain the standard boolean connectives and, in addition, , , , and , where and are expressions. The constant asserts that the heap is empty, i. e., when is undefined for all addresses. The binary operator takes an address and a value and asserts that the heap is defined at exactly one location, mapping the given address to the given value. I. e., when (where denotes the value of expression evaluated in store ) and is otherwise undefined. The binary operator (pronounced star or separating conjunction) asserts that the heap can be split into two disjoint parts where its two arguments hold, respectively. I. e., when there exist such that and and and The binary operator (pronounced magic wand or separating implication) asserts that extending the heap with a disjoint part that satisfies its first argument results in a heap that satisfies its second argument. I. e,. when for every heap such that , also holds. The operators and share some properties with the classical conjunction and implication operators. They can be combined using an inference rule similar to modus ponens

and they form an adjunction, i. e., if and only if for ; more precisely, the adjoint operators are and .

The satisfiability problem for a quantifier free, multi sorted fragment of separation logic parameterized over the sorts of locations and data can be shown to be PSPACE complete. An algorithm for solving this fragment in DPLL(T) based SMT solvers has been integrated into cvc5. Extending this result, satisfiability for an analog of the Bernays–Schönfinkel class for separation logic with uninterpreted memory locations can also be shown to be PSPACE complete, whereas the problem is undecidable with interpreted memory locations (e. g., integers) or further quantifier alternations