Invariants for Non-Hierarchical Object Structures

We present a Hoare-style specification and verification approach for invariants in sequential OO programs. It allows invariants over nonhierarchical object structures, in which update patterns that span several objects and methods occur frequently. This gives rise to invalidating and subsequent reestablishing of invariants in a way that compromises standard data induction, which assumes invariants hold when a method is called. We provide specification constructs (inc and coop) that identify objects and methods involved in such patterns, allowing a refined form of data induction. The approach now handles practical designs, as illustrated by a specification of the Observer Pattern.

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Ronald Middelkoop, Cornelis Huizing, Ruurd Kuiper, Erik J. Luit
• Keywords: Data Induction, ENTCS 2008, Sequential Oo Programs, Specification