6 CHAPTER 1.AN OVERVIEW 1.2 Background A partial bibliography of early work on reasoning about shared mutable data structure is given in Reference [1]. The central concept of separating conjunction is implicit in Burstall's early idea of a "distinct nonrepeating tree system"[2.In lectures in the fall of 1999,the author described the concept explicitly,and embedded it in a flawed extension of Hoare logic 3,4.Soon thereafter,a sound intuitionistic version of the logic was discovered independently by Ishtiag and O'Hearn 5]and by the author [1].Realizing that this logic was an instance of the separating implication PQ. The intuitionistic character of this logic implied a monotonicity property that an assertion true for some portion of the addressable storage would extension of that portion,such as might be created by in their paper.however.Ishtiaa and o'Hearn also presented a classical version of the logic that does not impose this monotonicity property,and can therefore be used to reason about explicit storage deallocation:they showed that this version is than the intuitionistic logic. since the latter can be translated into the classical logic O'Hearn also went on to devise the frame rule and illustrate its importance [8,9,10,5 Originally,in both the intuitionistic and classical version of the logic addresses were assumed to be disjoint from integers,and to refer to entire records rather than particular fields,so that address arithmetic was pre- cluded.Later,the author generalized the logic to permit reasoning about unrestricted address arithmetic,by regarding addresses as integers which re- fer to individual fields 8,11].It is this form of the logic that will be described and used in most of these note Since these logics are based on the idea that the structure of an assertion can describe the separation of storage into disjoint components,we have come to use the term separation logic,both for the extension of predicate calculus with the separation operators and for the resulting extension of Hoare logic At present,separation logic has been used to manually verify a variety of small programs,as well as a few that are large enough to demonstrate the potential of local reasoning for scalability [12,10,13,14,15].In addition: 6 CHAPTER 1. AN OVERVIEW 1.2 Background A partial bibliography of early work on reasoning about shared mutable data structure is given in Reference [1]. The central concept of separating conjunction is implicit in Burstall’s early idea of a “distinct nonrepeating tree system” [2]. In lectures in the fall of 1999, the author described the concept explicitly, and embedded it in a flawed extension of Hoare logic [3, 4]. Soon thereafter, a sound intuitionistic version of the logic was discovered independently by Ishtiaq and O’Hearn [5] and by the author [1]. Realizing that this logic was an instance of the logic of bunched implications [6, 7], Ishtiaq and O’Hearn also introduced a separating implication P −∗ Q. The intuitionistic character of this logic implied a monotonicity property: that an assertion true for some portion of the addressable storage would remain true for any extension of that portion, such as might be created by later storage allocation. In their paper, however, Ishtiaq and O’Hearn also presented a classical version of the logic that does not impose this monotonicity property, and can therefore be used to reason about explicit storage deallocation; they showed that this version is more expressive than the intuitionistic logic, since the latter can be translated into the classical logic. O’Hearn also went on to devise the frame rule and illustrate its importance [8, 9, 10, 5]. Originally, in both the intuitionistic and classical version of the logic, addresses were assumed to be disjoint from integers, and to refer to entire records rather than particular fields, so that address arithmetic was pre￾cluded. Later, the author generalized the logic to permit reasoning about unrestricted address arithmetic, by regarding addresses as integers which re￾fer to individual fields [8, 11]. It is this form of the logic that will be described and used in most of these notes. Since these logics are based on the idea that the structure of an assertion can describe the separation of storage into disjoint components, we have come to use the term separation logic, both for the extension of predicate calculus with the separation operators and for the resulting extension of Hoare logic. At present, separation logic has been used to manually verify a variety of small programs, as well as a few that are large enough to demonstrate the potential of local reasoning for scalability [12, 10, 13, 14, 15]. In addition: