An Introduction to Separation Logic 2008 John C.Reynolds October 23.2008 Chapter 1 An Overview Separation logic is a novel system for reasoning about imperative programs. It extends Hoare logic with enriched assertions that can describe the separa- tion of stor ources concisely.The original goal of the logic ed mutable data struct res,i.e.,stru tuere upatablebe rfren from more th one po! More recently,the logic has been extended to deal with shared-variable con- currency and information hiding,and the notion of separation has proven applicable to a wider conceptual range,where access to memory is replaced by permission to exercise capabilities,or by knowledge of structure.In a research area,with a growing 1.1 An Example of the Problem The use of shared mutable data structures is widespread in areas as diverse as systems programming and artificial intelligence.Approaches to reasoning about this technique have been studied for three decades,but the result has been methods that suffer from either limited applicability or extreme complexity,and scale poorly to programs of even moderate size. For co onventional logics,the problem with sharing is that it is the default in the logic hile nonsharing is the default in programming,so that decaring all of the instances where sharing does not occur-or at least those instances necessary for correctness-can be extremely tedious. For example,consider the following program,which performs an in-place 3Chapter 1 An Overview An Introduction to Separation Logic c 2008 John C. Reynolds October 23, 2008 Separation logic is a novel system for reasoning about imperative programs. It extends Hoare logic with enriched assertions that can describe the separa￾tion of storage and other resources concisely. The original goal of the logic was to facilitate reasoning about shared mutable data structures, i.e., struc￾tures where updatable fields can be referenced from more than one point. More recently, the logic has been extended to deal with shared-variable con￾currency and information hiding, and the notion of separation has proven applicable to a wider conceptual range, where access to memory is replaced by permission to exercise capabilities, or by knowledge of structure. In a few years, the logic has become a significant research area, with a growing literature produced by a variety of researchers. 1.1 An Example of the Problem The use of shared mutable data structures is widespread in areas as diverse as systems programming and artificial intelligence. Approaches to reasoning about this technique have been studied for three decades, but the result has been methods that suffer from either limited applicability or extreme complexity, and scale poorly to programs of even moderate size. For conventional logics, the problem with sharing is that it is the default in the logic, while nonsharing is the default in programming, so that declaring all of the instances where sharing does not occur — or at least those instances necessary for correctness — can be extremely tedious. For example, consider the following program, which performs an in-place 3