We investigate proof rules for information hiding, using the recent formalism of separation logic. In essence, we use the separating conjunction to partition
the internal resources of a module from those accessed by the module's clients.
The use of a logical connective gives rise to a form of dynamic partitioning,
where we track the transfer of ownership of portions of heap storage
between program components. It also enables us to enforce separation
in the presence of mutable data structures with embedded addresses
that may be aliased.
