Separation logic is an extension of Hoare?s logic which supports a local way of reasoning about programs that mutate memory. We present a study of the semantic structures lying behind the logic. The core idea is of a local action, a state transformer that mutates the state in a local way. We formulate local actions for a class of models called separation algebras, abstracting from the RAM and other specific concrete models used in work on separation logic. Local actions provide a semantics for a generalized form of (sequential) separation logic. We also show that our conditions on local actions allow a general soundness proof for a separation logic for concurrency, interpreted over arbitrary separation algebras.
Citation:
Cristiano Calcagno, Peter W. O'Hearn, Hongseok Yang, "Local Action and Abstract Separation Logic," lics, pp.366-378, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 2007