Class Invariants: Concepts, Problems, Solutions

TL;DR

This paper presents a modular approach to handling class invariants in object-oriented programming, addressing key verification problems without requiring additional language constructs or annotations.

Contribution

It introduces the O-rule and inhibition rule to solve invariants and reference leaks, and proposes the 'object tribe' concept for modular verification, all without new language features.

Findings

Addresses verification problems like furtive access and leaks

Provides a simple theory solving linked list and Observer invariants

No new language constructs or annotations required

Abstract

Class invariants are both a core concept of object-oriented programming and the source of the two key open OO verification problems: furtive access (from callbacks) and reference leak. Existing approaches force on programmers an unacceptable annotation burden. This article explains invariants and solves both problems modularly through the O-rule, defining fundamental OO semantics, and the inhibition rule, using information hiding to remove harmful reference leaks. It also introduces the concept of "object tribe" as a basis for other possible approaches. For all readers: this article is long because it includes a tutorial, covers many examples and dispels misconceptions. To understand the key ideas and results, however, the first two pages suffice. For non-experts in verification: all concepts are explained; anyone with a basic understanding of object-oriented programming can understand the discussion. For experts: the main limitation of this work is that it is a paper proposal (no soundness proof, no implementation). It addresses, however, the known problems with class invariants, solving such examples as linked lists and Observer, through a simple theory and without any of the following: ownership; separation logic; universe types; object wrapping and unwrapping; semantic collaboration, observer specifications; history invariants; "inc" and "coop" constructs; friendship construct; non-modular reasoning. More generally, it involves no new language construct and no new programmer annotations.