Using History Invariants to Verify Observers

Abstract. This paper contributes a technique that expands the set of object invariants that one can reason about in modular verification. The technique uses history invariants, two-state invariants that describe the evolution of data values. The technique enables a flexible new way to specify and verify variations of the observer pattern, including iterators. The paper details history invariants and the new kind of object invariants, and proves a soundness theorem.

• Type: Conference
• Year: 2007
• Where: ESOP
• Authors: K. Rustan M. Leino, Wolfram Schulte
• Keywords: ESOP 2007, History Invariants, Object Invariants, Programming Languages, Two-state Invariants