Authors
Gang Tan
Zhong Shao
Xinyu Feng
Hongxu Cai
Abstract
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 SL
W,
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 SL
W. Finally, we show how to
extend SL
W with concurrency.
Published
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
(APLAS'09),
Seoul, Korea, December 2009.
Lecture Notes in Computer Science Vol. 5904, pages 178-193.