Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions

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.

• Type: Conference
• Year: 2006
• Where: FM
• Authors: Ioannis T. Kassios
• Keywords: Dynamic Frames, FM 2006, Formal Methods, Frame Problem, Specification Variables