Friends Need a Bit More: Maintaining Invariants Over Shared State

A friendship system is introduced for modular static verification of object invariants. It extends a previous methodology, based on ownership hierarchy encoded in auxiliary state, to allow for state dependence across ownership boundaries. Friendship describes a formal protocol for a granting class to grant a friend class permission to express its invariant over fields in the granting class. The protocol permits the safe update of the granter’s fields without violating the friend’s invariant. The ensuing proof obligations are minimal and permit many common programming patterns. A soundness proof is sketched. The method is demonstrated on several realistic examples, showing that it significantly expands the domain of programs amenable to static verification.

• Type: Conference
• Year: 2004
• Where: MPC
• Authors: Michael Barnett, David A. Naumann
• Keywords: Friend Class Permission, Mathematics, Modular Static Verification, MPC 2004, Static Verification