Separation Logic (SL) provides a simple but powerful
technique for reasoning about imperative programs that use shared data
structures. Unfortunately, SL supports only ``strong updates,'' in
which mutation to a heap location is safe only if a unique reference
is owned. This limits the applicability of SL when reasoning about
the interaction between many high-level languages (e.g., ML, Java, C#)
and low-level ones since these high-level languages do not support
strong updates. Instead, they adopt the discipline of ``weak
updates,'' in which there is a global ``heap type'' to enforce the
invariant of type-preserving heap updates. We present SLW
a logic that extends SL with reference types and elegantly reasons
about the interaction between strong and weak updates. We also
describe a semantic framework for reference types, which is used
to prove the soundness of SLW
. Finally, we show how to
In New Generation Computing: Computing Paradigms and Computational Intelligence
, Volume 29, No. 1, 2011, pages 1-29.
© Ohmsha, Ltd. and Springer 2011.
An earlier version appeared in
Proc. 7th Asian Symposium on Programming Languages and Systems
Seoul, Korea, December 2009.
Lecture Notes in Computer Science Vol. 5904, pages 178-193.