Dynamic frames: Support for framing, dependencies and sharing without restrictions

Abstract

This paper addresses the frame problem for programming theories that support both sharing and encapsulation through specification variables. The concept of dynamic frames is introduced. It is shown how a programming theory with dynamic frames supports both features, without the use of alias control or any other kind of restriction. In contrast, other approaches introduce a number of restrictions to the programs to ensure soundness. © Springer-Verlag Berlin Heidelberg 2006.