1.1.AN EXAMPLE OF THE PROBLEM Even in this trivial situation,where all sharing is prohibited,it is evident that this form of reasoning scales poorly. In separation logic,however,this kind of difficulty can be avoided by using a novel logical operation P*Q,called the separating conjunction,that that P and Q hold for disjoint portions of the addre ssable storag ing is built into this operation,Invariant(1.1) can be written more succinctly as (3a,B.list a i list Bj)A ad =at.B, (1.3) and Invariant (1.2)as (3a,B.list a i list Bj list x)A ao=at.B. (1.4) A more general advantage is the support that separation logic gives to local reasoning,which underlies the scalability of the logic.For example,one can use (1.3)to prove a local specification: {list a i}LREV {list at j). In separation logic,this specification implies,not only that the program expects to find a list at i representing a,but also that this list is the only addressable storage touched by the execution of LREV(often called the foot- print of LREV).If LREV is a part of a larger program that also manipulates some separate storage,say containing the list k.then one can use an infer- ence rule due to O'Hear called the frame rule,to infer directly that the additional storage is unaffected byLR {list a i list yk}LREV {list at j list k}, thereby avoiding the extra complexity of Invariant(1.4). In a realistic situation,of course,LREV might be a substantial subpro- n.and the description n of the s eparate sto might also be volumine reaso locally about】 REV,i.e.,while ignoring the separate storage,and then scale up to the combined storage by using the frame rule. There is little need for local reasoning in proving toy examples.But it provides scalability that is critical for more complex programs.1.1. AN EXAMPLE OF THE PROBLEM 5 Even in this trivial situation, where all sharing is prohibited, it is evident that this form of reasoning scales poorly. In separation logic, however, this kind of difficulty can be avoided by using a novel logical operation P ∗ Q, called the separating conjunction, that asserts that P and Q hold for disjoint portions of the addressable storage. Since the prohibition of sharing is built into this operation, Invariant (1.1) can be written more succinctly as (∃α, β. list α i ∗ list β j) ∧ α † 0 = α † ·β, (1.3) and Invariant (1.2) as (∃α, β. list α i ∗ list β j ∗ list γ x) ∧ α † 0 = α † ·β. (1.4) A more general advantage is the support that separation logic gives to local reasoning, which underlies the scalability of the logic. For example, one can use (1.3) to prove a local specification: {list α i} LREV {list α † j}. In separation logic, this specification implies, not only that the program expects to find a list at i representing α, but also that this list is the only addressable storage touched by the execution of LREV (often called the foot￾print of LREV ). If LREV is a part of a larger program that also manipulates some separate storage, say containing the list k, then one can use an infer￾ence rule due to O’Hearn, called the frame rule, to infer directly that the additional storage is unaffected by LREV: {list α i ∗ list γ k} LREV {list α † j ∗ list γ k}, thereby avoiding the extra complexity of Invariant (1.4). In a realistic situation, of course, LREV might be a substantial subpro￾gram, and the description of the separate storage might also be voluminous. Nevertheless, one can still reason locally about LREV, i.e., while ignoring the separate storage, and then scale up to the combined storage by using the frame rule. There is little need for local reasoning in proving toy examples. But it provides scalability that is critical for more complex programs