| Research |
| [ CSI ] [ ETH ] |
[ Lab Manager ]
| [ Publications ] [ Research Opportunities ] [ Partners & Supporters ] [ Earlier Work ] |
|
Verifying Multi-Object Invariants with Relationships |
| Stephanie Balzer, Thomas R. GRoss, Verifying Multi-Object Invariants with Relationships, 25th European Conference on Object-Oriented Programming (ECOOP'11), Mira Mezini, Springer 2011. [ECOOP_2011.pdf] |
| 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. |
| [ Publications ] [ Research Opportunities ] [ Partners & Supporters ] [ Earlier Work ] |