Details

Autor(en) / Beteiligte

• Balzer, Stephanie
• Gross, Thomas R.

Titel

Verifying Multi-object Invariants with Relationships

Ist Teil von

• ECOOP 2011 – Object-Oriented Programming, p.358-382

Ort / Verlag

Berlin, Heidelberg: Springer Berlin Heidelberg

Link zum Volltext

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• 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.