?. , ?. , {. }. , and *. ==, 6) ?, ? ; r; F F (4.7) ?, ? ; r {F * == v}c : void{G} (4, )()), we have: (4.9) ?, ? s

R. ). Applying-resource-monotonicityr-ts and . We, we get: (9.21) R ts R ts : By resource axiom (d) for R ts , we know that (R ts ) loc (p, k) = 0 for all k in FieldId ? {join}. It follows that, By Lemma, vol.27, issue.7

*. R. We-have-(-r-ts and =. , ? (C< ¯ ?>, init(C< ¯ ?>))] = h . Thus, we can apply (State) to obtain: (9.23) h , ts | o is

?. Pointsto-or, ?. |=-pure, E. , R. , and ?. Pointsto, But neither of these statements hold, by definition of |=. Suppose now that hc = (fin null. f = v) An inspection of the last rules of (st : )'s derivation reveals that there must then be But this is false, by definition of |=. Suppose finally that hc = ( =null.m< ¯ ?>( ¯ v)). An inspection of the last rules of (st : )'s derivation reveals that there must then be ?, E , R, s such that ? E ; R; s |= null!= null

. Proof and . Let, st = h, ts | o is (s in assert(F); c), and init(c) ? * ct st By init(c) : (Lemma 93) and preservation (Theorem 5), we know that st : . An inspection of the last rules of (st : )'s derivation reveals

]. M. Abadi, C. Flanagan, and S. Freund, Types for safe locking, ACM Transactions on Programming Languages and Systems, vol.28, issue.2, 2006.
DOI : 10.1145/1119479.1119480

A. W. Appel and S. Blazy, Separation Logic for Small-Step cminor, TPHOL, 2007.
DOI : 10.1007/978-3-540-74591-4_3
URL : https://hal.archives-ouvertes.fr/inria-00165915

M. Barnett, R. Deline, M. Fähndrich, K. R. Leino, and W. Schulte, Verification of Object-Oriented Programs with Invariants., The Journal of Object Technology, vol.3, issue.6, 2004.
DOI : 10.5381/jot.2004.3.6.a2

J. Berdine, C. Calcagno, and P. W. O-'hearn, Smallfoot: Modular Automatic Assertion Checking with Separation Logic, FMCO, 2005.
DOI : 10.1007/11804192_6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.63.613

K. Bierhoff and J. Aldrich, Modular typestate verification of aliased objects, OOPSLA, 2007.

R. Bornat, P. O-'hearn, C. Calcagno, and M. Parkinson, Permission accounting in separation logic, POPL, 2005.

C. Boyapati, R. Lee, and M. Rinard, Ownership types for safe programming: Preventing data races and deadlocks, OOPSLA, 2002.

J. Boyland, Checking Interference with Fractional Permissions, LNCS, vol.2694, 2003.
DOI : 10.1007/3-540-44898-5_4

J. Boyland and W. Retert, Connecting effects and uniqueness with adoption, POPL, 2005.

S. Brookes, A semantics for concurrent separation logic, Conference on Concurrency Theory, 2004.

S. Brookes, Variables as Resource for Shared-Memory Programs: Semantics and Soundness, Electronic Notes in Theoretical Computer Science, vol.158, 2006.
DOI : 10.1016/j.entcs.2006.04.008

L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. R. Kiniry et al., An overview of JML tools and applications, Workshop on Formal Methods for Industrial Critical Systems, 2003.
DOI : 10.1007/s10009-004-0167-4

R. Deline and M. Fähndrich, Typestates for Objects, ECOOP, 2004.
DOI : 10.1007/978-3-540-24851-4_21

D. Distefano, P. W. O-'hearn, and H. Yang, A Local Shape Analysis Based on Separation Logic, TACAS, 2006.
DOI : 10.1145/514188.514190

A. Gotsman, J. Berdine, B. Cook, N. Rinetzky, and M. Sagiv, Local Reasoning for Storable Locks and Threads, APLAS, 2007.
DOI : 10.1007/978-3-540-76637-7_3

A. Igarashi, B. Pierce, and P. Wadler, Featherweight Java: a minimal core calculus for Java and GJ, ACM Transactions on Programming Languages and Systems, vol.23, issue.3, 2001.
DOI : 10.1145/503502.503505

S. Ishtiaq and P. O. Hearn, BI as an assertion language for mutable data structures, POPL, 2001.

B. Jacobs, J. Smans, F. Piessens, and W. Schulte, A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs, ICFEM, 2006.
DOI : 10.1007/11901433_23

G. Krishnaswami, Reasoning about iterators with separation logic, Proceedings of the 2006 conference on Specification and verification of component-based systems , SAVCBS '06, 2006.
DOI : 10.1145/1181195.1181213

D. Lea, Concurrent Programming in Java: Design Principles and Patterns, 1999.

G. T. Leavens, E. Poll, C. Clifton, Y. Cheon, C. Ruby et al., Available from http, Progress, 2005.

K. R. Leino, Data groups: Specifying the modification of extended state, OOPSLA, 1998.

J. Manson, W. Pugh, and S. V. Adve, The Java memory model, POPL, 2005.

P. O. Hearn, Resources, concurrency and local reasoning, TCS, vol.375, pp.1-3, 2007.

P. W. O-'hearn and D. J. Pym, The logic of bunched implications, Bulletin of Symbolic Logic, vol.5, issue.2, 1999.

M. Parkinson, Local reasoning for Java, 2005.

M. Parkinson and G. Bierman, Separation logic and abstraction, POPL, 2005.
DOI : 10.1145/1040305.1040326
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.59.5332

M. Pavlova, G. Barthe, L. Burdy, M. Huisman, and J. Lanet, Enforcing High-Level Security Properties for Applets, 2004.
DOI : 10.1007/1-4020-8147-2_1
URL : https://hal.archives-ouvertes.fr/inria-00071523

J. C. Reynolds, Separation logic: a logic for shared mutable data structures, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, 2002.
DOI : 10.1109/LICS.2002.1029817

J. C. Reynolds, Toward a Grainless Semantics for Shared-Variable Concurrency, FSTTCS LNCS, vol.3328, 2004.
DOI : 10.1007/978-3-540-30538-5_4

P. Wadler, A taste of linear logic, Mathematical Foundations of Computer Science, 1993.
DOI : 10.1007/3-540-57182-5_12

H. Yang, An example of local reasoning in BI pointer logic: the Schorr-Waite graph marking algorithm, SPACE, 2001.