Separation logic
Encyclopedia
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 Burstall. The assertion language of separation logic is a special case of the logic of bunched implications (BI).
Separation logic facilitates reasoning about:
Separation logic supports the developing field of research described by Peter O'Hearn
and others as local reasoning, whereby specifications and proofs of a program component mention only the portion of memory used by the component, and not the entire global state of the system. Applications include automated program verification (where an algorithm
checks the validity of another algorithm) and automated parallelization of software.
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., if 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 
as expressions.
The operators
and 
share some properties in common 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 triple
asserts that if the program, 
, executes from an initial state satisfying the precondition, 
, then the program will not go wrong (e.g., have undefined behaviour), and if it terminates, then the final state will satisfy the postcondition, 
. In essence, during its execution, 
may access only memory locations whose existence is asserted in the precondition or that have been allocated by 
itself.
In addition to the standard rules from Hoare logic
, separation logic supports the following very important rule:
This is known as the frame rule and enables local reasoning. It says that a program that executes safely in a small state (satisfying
), can also execute in any bigger state (satisfying 
) and that its execution will not affect the additional part of the state (and so 
will remain true in the postcondition).
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, separation logic is an extension of Hoare logic
Hoare logic
Hoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers...
, a way of reasoning about programs.
It was developed by John C. Reynolds
John C. Reynolds
John C. Reynolds is an American computer scientist.John Reynolds studied at Purdue University and then earned a PhD in theoretical physics from Harvard University in 1961. He was Professor of Information science at Syracuse University from 1970 to 1986. Since then he has been Professor of Computer...
, Peter O'Hearn
Peter O'Hearn
Peter William O'Hearn is a computer scientist based in the United Kingdom.Peter O'Hearn attained a BSc degree in Computer Science from Dalhousie University, Halifax, Nova Scotia , followed by MSc and PhD degrees fromQueen's University, Kingston, Ontario, Canada...
, Samin Ishtiaq and Hongseok Yang, drawing upon early work by Burstall. The assertion language of separation logic is a special case of the logic of bunched implications (BI).
Separation logic facilitates reasoning about:
- programs that manipulate pointer data structures — including information hidingInformation hidingIn computer science, information hiding is the principle of segregation of the design decisions in a computer program that are most likely to change, thus protecting other parts of the program from extensive modification if the design decision is changed...
in the presence of pointers; - "transfer of ownership" (avoidance of semantic frame axiomAxiomIn traditional logic, an axiom or postulate is a proposition that is not proven or demonstrated but considered either to be self-evident or to define and delimit the realm of analysis. In other words, an axiom is a logical statement that is assumed to be true...
s); and - virtual separation (modular reasoning) between concurrent modules.
Separation logic supports the developing field of research described by Peter O'Hearn
Peter O'Hearn
Peter William O'Hearn is a computer scientist based in the United Kingdom.Peter O'Hearn attained a BSc degree in Computer Science from Dalhousie University, Halifax, Nova Scotia , followed by MSc and PhD degrees fromQueen's University, Kingston, Ontario, Canada...
and others as local reasoning, whereby specifications and proofs of a program component mention only the portion of memory used by the component, and not the entire global state of the system. Applications include automated program verification (where an algorithm
Algorithm
In mathematics and computer science, an algorithm is an effective method expressed as a finite list of well-defined instructions for calculating a function. Algorithms are used for calculation, data processing, and automated reasoning...
checks the validity of another algorithm) and automated parallelization of software.
Assertions: Operators and semantics
Separation logic assertion describe "states" consisting of a store and a heap, roughly corresponding to the state of local (or stack-allocated) variablesStack-based memory allocation
Stacks in computing architectures are regions of memory where data is added or removed in a last-in-first-out manner.In most modern computer systems, each thread has a reserved region of memory referred to as its stack. When a function executes, it may add some of its state data to the top of the...
and dynamically-allocated objects in common programming languages such as C
C (programming language)
C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....
and Java
Java (programming language)
Java is a programming language originally developed by James Gosling at Sun Microsystems and released in 1995 as a core component of Sun Microsystems' Java platform. The language derives much of its syntax from C and C++ but has a simpler object model and fewer low-level facilities...
. A store
is a functionFunction (mathematics)
In mathematics, a function associates one quantity, the argument of the function, also known as the input, with another quantity, the value of the function, also known as the output. A function assigns exactly one output to each input. The argument and the value may be real numbers, but they can...
mapping variables to values. A heap
is a partial functionPartial function
In mathematics, a partial function from X to Y is a function ƒ: X' → Y, where X' is a subset of X. It generalizes the concept of a function by not forcing f to map every element of X to an element of Y . If X' = X, then ƒ is called a total function and is equivalent to a function...
mapping memory addresses to values. Two heaps
and are disjoint (denoted ) if their domains do not overlap (i.e., if 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 as 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
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
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 any heap 
such that 
, we also have 
.
The operators
and share some properties in common with the classical conjunctionLogical conjunction
In logic and mathematics, a two-place logical operator and, also known as logical conjunction, results in true if both of its operands are true, otherwise the value of false....
and implication
Entailment
In logic, entailment is a relation between a set of sentences and a sentence. Let Γ be a set of one or more sentences; let S1 be the conjunction of the elements of Γ, and let S2 be a sentence: then, Γ entails S2 if and only if S1 and not-S2 are logically inconsistent...
operators. They can be combined using an inference rule similar to modus ponens
Modus ponens
In classical logic, modus ponendo ponens or implication elimination is a valid, simple argument form. It is related to another valid form of argument, modus tollens. Both Modus Ponens and Modus Tollens can be mistakenly used when proving arguments...
and they form an adjunction, i.e.,
if and only if for ; more precisely, the adjoint operators are and .Reasoning about programs: triples & proof rules
In separation logic, Hoare triples have a slightly different meaning than in Hoare logicHoare logic
Hoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers...
. The triple
asserts that if the program, , executes from an initial state satisfying the precondition, , then the program will not go wrong (e.g., have undefined behaviour), and if it terminates, then the final state will satisfy the postcondition, . In essence, during its execution, may access only memory locations whose existence is asserted in the precondition or that have been allocated by itself.In addition to the standard rules from Hoare logic
Hoare logic
Hoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers...
, separation logic supports the following very important rule:
This is known as the frame rule and enables local reasoning. It says that a program that executes safely in a small state (satisfying
), can also execute in any bigger state (satisfying ) and that its execution will not affect the additional part of the state (and so will remain true in the postcondition).