Abstract

The object invariant has proved viable as a foundation for verifying object-oriented programs and is central to a wealth of object-oriented verification techniques. However, the presence of multi-object invariants and call-backs poses serious challenges for object invariant-based verification as they compromise modular verification and prohibit a naive adoption of a visible states semantics.

In this talk, we introduce Rumer, a relationship-based programming language that complements objects with first-class relationships. A relationship is a programming language abstraction that captures the interdependencies between objects. We discuss how relationships can aid in the modular verification of multi-object invariants. We introduce the “Matryoshka Principle”, a metaphor capturing Rumer’s key encapsulation properties that make the language amenable to modular verification. The principle stipulates restrictions on field and method access that translate into a stratification of the invariants imposed on a Rumer program. A verification technique can now leverage the invariant stratification as it allows restoring a visible states semantics for multi-object invariants. We elaborated a visible states verification technique for Rumer, which we outline in this talk.