Verifying Multi-object Invariants with Relationships

Relationships capture the interplay between classes in object-oriented programs, and various extensions of object-oriented programming languages allow the programmer to explicitly express relationships. This paper discusses how relationships facilitate the verification of multi-object invariants. We develop a visible states verification technique for Rumer, a relationship-based programming language, and demonstrate our technique on the Composite pattern. The verification technique leverages the “Matryoshka Principle” embodied in the Rumer language: relationships impose a stratification of classes and relationships (with corresponding restrictions on writes to fields, the expression of invariants, and method invocations). The Matryoshka Principle guarantees the absence of transitive call-backs and restores a visible states semantics for multi-object invariants. As a consequence, the modular verification of multi-object invariants is possible.

• Type: Journal
• Year: 2011
• Where: ECOOP
• Authors: Stephanie Balzer, Thomas R. Gross
• Keywords: ECOOP 2011, Language Relationships, Object Oriented Programming Languages, Oriented Programming Languages, Programming Languages